Let h be given.
Assume HhR: ∀i : set, i ∈ ω → h i ∈ R.
We will prove graph ω h ∈ R_omega_space.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set U0 to be the term space_family_union ω Xi.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HXi0: apply_fun Xi 0 = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology 0 H0omega).
We prove the intermediate claim Hset0: space_family_set Xi 0 = R.
We prove the intermediate claim Hdef: space_family_set Xi 0 = (apply_fun Xi 0) 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi0 (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
We prove the intermediate claim HRfam: R ∈ {space_family_set Xi i|i ∈ ω}.
Apply ReplEq ω (λi : set ⇒ space_family_set Xi i) R to the current goal.
Assume _ H2.
Apply H2 to the current goal.
We will prove ∃i ∈ ω, R = space_family_set Xi i.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H0omega.
We will prove R = space_family_set Xi 0.
Use symmetry.
An exact proof term for the current goal is Hset0.
We prove the intermediate claim HRinU0: ∀r : set, r ∈ R → r ∈ U0.
Let r be given.
Assume Hr: r ∈ R.
An exact proof term for the current goal is (UnionI {space_family_set Xi i|i ∈ ω} r R Hr HRfam).
We prove the intermediate claim Hsub: graph ω h ⊆ setprod ω U0.
Let p be given.
Assume Hp: p ∈ graph ω h.
We will prove p ∈ setprod ω U0.
Apply (ReplE_impred ω (λi : set ⇒ (i,h i)) p Hp (p ∈ setprod ω U0)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Assume Heq: p = (i,h i).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HhiR: h i ∈ R.
An exact proof term for the current goal is (HhR i Hi).
We prove the intermediate claim HhiU0: h i ∈ U0.
An exact proof term for the current goal is (HRinU0 (h i) HhiR).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω U0 i (h i) Hi HhiU0).
We prove the intermediate claim Hpow: graph ω h ∈ 𝒫 (setprod ω U0).
An exact proof term for the current goal is (PowerI (setprod ω U0) (graph ω h) Hsub).
We prove the intermediate claim Hfun: function_on (graph ω h) ω U0.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun (graph ω h) i ∈ U0.
We prove the intermediate claim Happ: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (HRinU0 (h i) (HhR i Hi)).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ ω → apply_fun (graph ω h) i ∈ space_family_set Xi i.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun (graph ω h) i ∈ space_family_set Xi i.
We prove the intermediate claim Happ: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HXi: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).
We prove the intermediate claim Hset: space_family_set Xi i = R.
We prove the intermediate claim Hdef: space_family_set Xi i = (apply_fun Xi i) 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
rewrite the current goal using Hset (from left to right).
An exact proof term for the current goal is (HhR i Hi).
We prove the intermediate claim Htot: total_function_on (graph ω h) ω U0.
We prove the intermediate claim Htot': ∀i : set, i ∈ ω → ∃y : set, y ∈ U0 ∧ (i,y) ∈ graph ω h.
Let i be given.
Assume Hi: i ∈ ω.
We use (h i) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HRinU0 (h i) (HhR i Hi)).
An exact proof term for the current goal is (ReplI ω (λa : set ⇒ (a,h a)) i Hi).
An exact proof term for the current goal is (andI (function_on (graph ω h) ω U0) (∀x : set, x ∈ ω → ∃y : set, y ∈ U0 ∧ (x,y) ∈ graph ω h) Hfun Htot').
We prove the intermediate claim Hgraph: functional_graph (graph ω h).
An exact proof term for the current goal is (functional_graph_graph ω h).
We prove the intermediate claim Hprop: total_function_on (graph ω h) ω U0 ∧ functional_graph (graph ω h) ∧ ∀i : set, i ∈ ω → apply_fun (graph ω h) i ∈ space_family_set Xi i.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Htot.
An exact proof term for the current goal is Hgraph.
An exact proof term for the current goal is Hcoords.
An exact proof term for the current goal is (SepI (𝒫 (setprod ω U0)) (λf0 : set ⇒ total_function_on f0 ω U0 ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i) (graph ω h) Hpow Hprop).
∎