We will prove closure_of (Romega_tilde 0) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde 0)) (image_of Romega_singleton_map R) = Romega_tilde 0.
Set X to be the term R_omega_space.
Set Tx to be the term R_omega_product_topology.
Set Y to be the term Romega_tilde 0.
Set A to be the term image_of Romega_singleton_map R.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (Romega_tilde_sub_Romega 0).
We prove the intermediate claim HAsubY: A ⊆ Y.
An exact proof term for the current goal is image_of_Romega_singleton_map_sub_Romega_tilde0.
We prove the intermediate claim HclEq: closure_of Y (subspace_topology X Tx Y) A = (closure_of X Tx A) ∩ Y.
An exact proof term for the current goal is (closure_in_subspace X Tx Y A HTx HYsub HAsubY).
rewrite the current goal using HclEq (from left to right).
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ (closure_of X Tx A) ∩ Y.
An exact proof term for the current goal is (binintersectE2 (closure_of X Tx A) Y z Hz).
Let y be given.
Assume Hy: y ∈ Y.
We will prove y ∈ (closure_of X Tx A) ∩ Y.
Apply binintersectI to the current goal.
We will prove y ∈ closure_of X Tx A.
We prove the intermediate claim HyCond: ∀U : set, U ∈ Tx → y ∈ U → U ∩ A ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HyU: y ∈ U.
We will prove U ∩ A ≠ Empty.
Set S to be the term product_subbasis_full ω (const_space_family ω R R_standard_topology).
Set B to be the term basis_of_subbasis X S.
We prove the intermediate claim HUl: ∀z ∈ U, ∃b0 ∈ B, z ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀z ∈ U0, ∃b0 ∈ B, z ∈ b0 ∧ b0 ⊆ U0) U HU).
Apply (HUl y HyU) to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B: b0 ∈ B.
An exact proof term for the current goal is (andEL (b0 ∈ B) (y ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hyb0sub: y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ B) (y ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hyb0: y ∈ b0.
An exact proof term for the current goal is (andEL (y ∈ b0) (b0 ⊆ U) Hyb0sub).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (y ∈ b0) (b0 ⊆ U) Hyb0sub).
We prove the intermediate claim Hb0neA: b0 ∩ A ≠ Empty.
An exact proof term for the current goal is (Romega_tilde0_meets_product_basis b0 y Hb0B Hy Hyb0).
Assume HUAempty: U ∩ A = Empty.
We prove the intermediate claim Hb0A_sub: b0 ∩ A ⊆ U ∩ A.
Let z be given.
Assume Hz: z ∈ b0 ∩ A.
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 A z Hz).
We prove the intermediate claim HzA: z ∈ A.
An exact proof term for the current goal is (binintersectE2 b0 A z Hz).
We prove the intermediate claim HzU0: z ∈ U.
An exact proof term for the current goal is (Hb0subU z Hzb0).
An exact proof term for the current goal is (binintersectI U A z HzU0 HzA).
We prove the intermediate claim Hb0A_empty: b0 ∩ A = Empty.
Apply Empty_Subq_eq to the current goal.
We prove the intermediate claim HUAE: U ∩ A ⊆ Empty.
rewrite the current goal using HUAempty (from left to right).
An exact proof term for the current goal is (Subq_ref Empty).
An exact proof term for the current goal is (Subq_tra (b0 ∩ A) (U ∩ A) Empty Hb0A_sub HUAE).
An exact proof term for the current goal is (Hb0neA Hb0A_empty).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) y (HYsub y Hy) HyCond).
An exact proof term for the current goal is Hy.
∎