We will prove Romega_zero ∈ 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 HR0: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HX0: 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 HX0 (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 H0U0: 0 ∈ U0.
An exact proof term for the current goal is (UnionI {space_family_set Xi i|i ∈ ω} 0 R HR0 HRfam).
We will prove Romega_zero ∈ product_space ω Xi.
We will prove Romega_zero ∈ {f ∈ 𝒫 (setprod ω (space_family_union ω Xi))|total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i}.
We prove the intermediate claim Hsub: Romega_zero ⊆ setprod ω U0.
Let p be given.
Assume Hp: p ∈ Romega_zero.
We will prove p ∈ setprod ω U0.
Apply (ReplE_impred ω (λa : set ⇒ (a,0)) p Hp (p ∈ setprod ω U0)) to the current goal.
Let a be given.
Assume HaO: a ∈ ω.
Assume Hpeq: p = (a,0).
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω U0 a 0 HaO H0U0).
We prove the intermediate claim Hpow: Romega_zero ∈ 𝒫 (setprod ω U0).
An exact proof term for the current goal is (PowerI (setprod ω U0) Romega_zero Hsub).
We prove the intermediate claim Htot: total_function_on Romega_zero ω U0.
An exact proof term for the current goal is (const_fun_total_function_on ω U0 0 H0U0).
We prove the intermediate claim Hgraph: functional_graph Romega_zero.
An exact proof term for the current goal is (functional_graph_const_fun ω 0).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ ω → apply_fun Romega_zero i ∈ space_family_set Xi i.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun Romega_zero i ∈ space_family_set Xi i.
We prove the intermediate claim Happ: apply_fun Romega_zero i = 0.
An exact proof term for the current goal is (const_fun_apply ω 0 i Hi).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HX: 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 HX (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 real_0.
We prove the intermediate claim Hprop: total_function_on Romega_zero ω U0 ∧ functional_graph Romega_zero ∧ ∀i : set, i ∈ ω → apply_fun Romega_zero 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)) (λf : set ⇒ total_function_on f ω U0 ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i) Romega_zero Hpow Hprop).
∎