Let f and g be given.
Assume HfX: f ∈ R_omega_space.
Assume HgX: g ∈ R_omega_space.
Assume Hcoord: ∀i : set, i ∈ ω → apply_fun f i = apply_fun g i.
We will prove f = g.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ f.
We will prove p ∈ g.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set Y to be the term space_family_union ω Xi.
We prove the intermediate claim HfPow: f ∈ 𝒫 (setprod ω Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) f HfX).
We prove the intermediate claim HgPow: g ∈ 𝒫 (setprod ω Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) g HgX).
We prove the intermediate claim Hfsub: f ⊆ setprod ω Y.
An exact proof term for the current goal is (PowerE (setprod ω Y) f HfPow).
We prove the intermediate claim Hgsub: g ⊆ setprod ω Y.
An exact proof term for the current goal is (PowerE (setprod ω Y) g HgPow).
We prove the intermediate claim HpProd: p ∈ setprod ω Y.
An exact proof term for the current goal is (Hfsub p Hp).
We prove the intermediate claim Hpeq: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta ω Y p HpProd).
Set i to be the term p 0.
Set y to be the term p 1.
We prove the intermediate claim Hip: i ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ Y) p HpProd).
We prove the intermediate claim Hfprop: (total_function_on f ω Y ∧ functional_graph f) ∧ ∀j : set, j ∈ ω → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) f HfX).
We prove the intermediate claim Hgprop: (total_function_on g ω Y ∧ functional_graph g) ∧ ∀j : set, j ∈ ω → apply_fun g j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) g HgX).
We prove the intermediate claim HfAB: total_function_on f ω Y ∧ functional_graph f.
An exact proof term for the current goal is (andEL (total_function_on f ω Y ∧ functional_graph f) (∀j : set, j ∈ ω → apply_fun f j ∈ space_family_set Xi j) Hfprop).
We prove the intermediate claim HgAB: total_function_on g ω Y ∧ functional_graph g.
An exact proof term for the current goal is (andEL (total_function_on g ω Y ∧ functional_graph g) (∀j : set, j ∈ ω → apply_fun g j ∈ space_family_set Xi j) Hgprop).
We prove the intermediate claim Htotg: total_function_on g ω Y.
An exact proof term for the current goal is (andEL (total_function_on g ω Y) (functional_graph g) HgAB).
We prove the intermediate claim Hfunf: functional_graph f.
An exact proof term for the current goal is (andER (total_function_on f ω Y) (functional_graph f) HfAB).
We prove the intermediate claim Hiyf: (i,y) ∈ f.
rewrite the current goal using Hpeq (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Happfy: apply_fun f i = y.
An exact proof term for the current goal is (functional_graph_apply_fun_eq f i y Hfunf Hiyf).
We prove the intermediate claim Happgi: apply_fun g i = y.
rewrite the current goal using (Hcoord i Hip) (from right to left).
An exact proof term for the current goal is Happfy.
We prove the intermediate claim Hexg: ∃y0 : set, (i,y0) ∈ g.
We prove the intermediate claim Hex0: ∃y0 : set, y0 ∈ Y ∧ (i,y0) ∈ g.
An exact proof term for the current goal is (total_function_on_totality g ω Y Htotg i Hip).
Apply Hex0 to the current goal.
Let y0 be given.
Assume Hy0.
We use y0 to witness the existential quantifier.
An exact proof term for the current goal is (andER (y0 ∈ Y) ((i,y0) ∈ g) Hy0).
We prove the intermediate claim Hpairg: (i,apply_fun g i) ∈ g.
An exact proof term for the current goal is (apply_fun_in_graph_of_ex g i Hexg).
We prove the intermediate claim Hiyg: (i,y) ∈ g.
rewrite the current goal using Happgi (from right to left).
An exact proof term for the current goal is Hpairg.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is Hiyg.
Let p be given.
Assume Hp: p ∈ g.
We will prove p ∈ f.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set Y to be the term space_family_union ω Xi.
We prove the intermediate claim HfPow: f ∈ 𝒫 (setprod ω Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) f HfX).
We prove the intermediate claim HgPow: g ∈ 𝒫 (setprod ω Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) g HgX).
We prove the intermediate claim Hfsub: f ⊆ setprod ω Y.
An exact proof term for the current goal is (PowerE (setprod ω Y) f HfPow).
We prove the intermediate claim Hgsub: g ⊆ setprod ω Y.
An exact proof term for the current goal is (PowerE (setprod ω Y) g HgPow).
We prove the intermediate claim HpProd: p ∈ setprod ω Y.
An exact proof term for the current goal is (Hgsub p Hp).
We prove the intermediate claim Hpeq: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta ω Y p HpProd).
Set i to be the term p 0.
Set y to be the term p 1.
We prove the intermediate claim Hip: i ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ Y) p HpProd).
We prove the intermediate claim Hfprop: (total_function_on f ω Y ∧ functional_graph f) ∧ ∀j : set, j ∈ ω → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) f HfX).
We prove the intermediate claim Hgprop: (total_function_on g ω Y ∧ functional_graph g) ∧ ∀j : set, j ∈ ω → apply_fun g j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω Y)) (λf0 : set ⇒ total_function_on f0 ω Y ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) g HgX).
We prove the intermediate claim HfAB: total_function_on f ω Y ∧ functional_graph f.
An exact proof term for the current goal is (andEL (total_function_on f ω Y ∧ functional_graph f) (∀j : set, j ∈ ω → apply_fun f j ∈ space_family_set Xi j) Hfprop).
We prove the intermediate claim HgAB: total_function_on g ω Y ∧ functional_graph g.
An exact proof term for the current goal is (andEL (total_function_on g ω Y ∧ functional_graph g) (∀j : set, j ∈ ω → apply_fun g j ∈ space_family_set Xi j) Hgprop).
We prove the intermediate claim Htotf: total_function_on f ω Y.
An exact proof term for the current goal is (andEL (total_function_on f ω Y) (functional_graph f) HfAB).
We prove the intermediate claim Hfung: functional_graph g.
An exact proof term for the current goal is (andER (total_function_on g ω Y) (functional_graph g) HgAB).
We prove the intermediate claim Hiyg: (i,y) ∈ g.
rewrite the current goal using Hpeq (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Happgy: apply_fun g i = y.
An exact proof term for the current goal is (functional_graph_apply_fun_eq g i y Hfung Hiyg).
We prove the intermediate claim Happfi: apply_fun f i = y.
rewrite the current goal using (Hcoord i Hip) (from left to right).
An exact proof term for the current goal is Happgy.
We prove the intermediate claim Hexf: ∃y0 : set, (i,y0) ∈ f.
We prove the intermediate claim Hex0: ∃y0 : set, y0 ∈ Y ∧ (i,y0) ∈ f.
An exact proof term for the current goal is (total_function_on_totality f ω Y Htotf i Hip).
Apply Hex0 to the current goal.
Let y0 be given.
Assume Hy0.
We use y0 to witness the existential quantifier.
An exact proof term for the current goal is (andER (y0 ∈ Y) ((i,y0) ∈ f) Hy0).
We prove the intermediate claim Hpairf: (i,apply_fun f i) ∈ f.
An exact proof term for the current goal is (apply_fun_in_graph_of_ex f i Hexf).
We prove the intermediate claim Hiyf: (i,y) ∈ f.
rewrite the current goal using Happfi (from right to left).
An exact proof term for the current goal is Hpairf.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is Hiyf.
∎