Set Xi to be the term const_space_family ω R R_standard_topology.
Apply set_ext to the current goal.
Let y be given.
Assume HyU: y ∈ space_family_union ω Xi.
We will prove y ∈ R.
Set S to be the term {space_family_set Xi i|i ∈ ω}.
Apply (UnionE_impred S y HyU (y ∈ R)) to the current goal.
Let U be given.
Assume HyUin: y ∈ U.
Assume HUin: U ∈ S.
Apply (ReplE_impred ω (λi : set ⇒ space_family_set Xi i) U HUin (y ∈ R)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume HUi: U = space_family_set Xi i.
We prove the intermediate claim HySf: y ∈ space_family_set Xi i.
We will prove y ∈ space_family_set Xi i.
rewrite the current goal using HUi (from right to left).
An exact proof term for the current goal is HyUin.
rewrite the current goal using (space_family_set_const_Romega i HiO) (from right to left).
An exact proof term for the current goal is HySf.
Let y be given.
Assume HyR: y ∈ R.
We will prove y ∈ space_family_union ω Xi.
Set S to be the term {space_family_set Xi i|i ∈ ω}.
We will prove y ∈ ⋃ S.
We prove the intermediate claim H0O: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HUin: space_family_set Xi 0 ∈ S.
An exact proof term for the current goal is (ReplI ω (λi : set ⇒ space_family_set Xi i) 0 H0O).
We prove the intermediate claim HyU0: y ∈ space_family_set Xi 0.
rewrite the current goal using (space_family_set_const_Romega 0 H0O) (from left to right).
An exact proof term for the current goal is HyR.
An exact proof term for the current goal is (UnionI S y (space_family_set Xi 0) HyU0 HUin).
∎