Let I, Xi, i, V and U be given.
Assume HIne: I ≠ Empty.
Assume HcompTop: ∀j : set, j ∈ I → topology_on (space_family_set Xi j) (space_family_topology Xi j).
Assume HiI: i ∈ I.
Assume HV: V ∈ space_family_topology Xi i.
Assume HU: U ∈ space_family_topology Xi i.
Assume HclVsubU: closure_of (space_family_set Xi i) (space_family_topology Xi i) V ⊆ U.
Set X to be the term product_space I Xi.
Set T to be the term product_topology_full I Xi.
Set S to be the term product_subbasis_full I Xi.
We will prove closure_of X T (product_cylinder I Xi i V) ⊆ product_cylinder I Xi i U.
We prove the intermediate claim HSsub: subbasis_on X S.
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIne HcompTop).
We prove the intermediate claim HT: topology_on X T.
An exact proof term for the current goal is (topology_from_subbasis_is_topology X S HSsub).
Let f be given.
Assume Hfcl: f ∈ closure_of X T (product_cylinder I Xi i V).
We will prove f ∈ product_cylinder I Xi i U.
We prove the intermediate claim HfX: f ∈ X.
An exact proof term for the current goal is (closure_in_space X T (product_cylinder I Xi i V) HT f Hfcl).
Apply (xm (apply_fun f i ∈ U)) to the current goal.
Assume HfiU: apply_fun f i ∈ U.
We prove the intermediate claim HdefCylU: product_cylinder I Xi i U = {g ∈ X|i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.
Use reflexivity.
rewrite the current goal using HdefCylU (from left to right).
We prove the intermediate claim Hprop: i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HiI.
An exact proof term for the current goal is HU.
An exact proof term for the current goal is HfiU.
An exact proof term for the current goal is (SepI X (λg : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f HfX Hprop).
Assume HfiNotU: apply_fun f i ∉ U.
Apply FalseE to the current goal.
We prove the intermediate claim Htopi: topology_on (space_family_set Xi i) (space_family_topology Xi i).
An exact proof term for the current goal is (HcompTop i HiI).
We prove the intermediate claim HTsub: (space_family_topology Xi i) ⊆ 𝒫 (space_family_set Xi i).
An exact proof term for the current goal is (topology_subset_axiom (space_family_set Xi i) (space_family_topology Xi i) Htopi).
We prove the intermediate claim HVsubXi: V ⊆ space_family_set Xi i.
An exact proof term for the current goal is (PowerE (space_family_set Xi i) V (HTsub V HV)).
We prove the intermediate claim Hfprop: total_function_on f I (space_family_union I Xi) ∧ functional_graph f ∧ ∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λg : set ⇒ total_function_on g I (space_family_union I Xi) ∧ functional_graph g ∧ ∀j : set, j ∈ I → apply_fun g j ∈ space_family_set Xi j) f HfX).
We prove the intermediate claim Hcoords: ∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (andER (total_function_on f I (space_family_union I Xi) ∧ functional_graph f) (∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j) Hfprop).
We prove the intermediate claim Hxcoord: apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (Hcoords i HiI).
We prove the intermediate claim HfiNotClV: apply_fun f i ∉ closure_of (space_family_set Xi i) (space_family_topology Xi i) V.
Assume HfiClV: apply_fun f i ∈ closure_of (space_family_set Xi i) (space_family_topology Xi i) V.
An exact proof term for the current goal is (HfiNotU (HclVsubU (apply_fun f i) HfiClV)).
We prove the intermediate claim HexW: ∃W : set, W ∈ space_family_topology Xi i ∧ apply_fun f i ∈ W ∧ W ∩ V = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open (space_family_set Xi i) (space_family_topology Xi i) V (apply_fun f i) Htopi HVsubXi Hxcoord HfiNotClV).
Apply HexW to the current goal.
Let W be given.
Assume HWconj.
We prove the intermediate claim HWcore: W ∈ space_family_topology Xi i ∧ apply_fun f i ∈ W.
An exact proof term for the current goal is (andEL (W ∈ space_family_topology Xi i ∧ apply_fun f i ∈ W) (W ∩ V = Empty) HWconj).
We prove the intermediate claim HWdisj: W ∩ V = Empty.
An exact proof term for the current goal is (andER (W ∈ space_family_topology Xi i ∧ apply_fun f i ∈ W) (W ∩ V = Empty) HWconj).
We prove the intermediate claim HW0: W ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (W ∈ space_family_topology Xi i) (apply_fun f i ∈ W) HWcore).
We prove the intermediate claim HfiW: apply_fun f i ∈ W.
An exact proof term for the current goal is (andER (W ∈ space_family_topology Xi i) (apply_fun f i ∈ W) HWcore).
Set N to be the term product_cylinder I Xi i W.
We prove the intermediate claim HNsub: N ∈ S.
We will prove N ∈ (⋃j ∈ I{product_cylinder I Xi j U0|U0 ∈ space_family_topology Xi j}).
Apply (famunionI I (λj : set ⇒ {product_cylinder I Xi j U0|U0 ∈ space_family_topology Xi j}) i N HiI) to the current goal.
An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder I Xi i U0) W HW0).
We prove the intermediate claim HNopen: N ∈ T.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X S N HSsub HNsub).
We prove the intermediate claim HfN: f ∈ N.
We prove the intermediate claim HdefCylW: N = {g ∈ X|i ∈ I ∧ W ∈ space_family_topology Xi i ∧ apply_fun g i ∈ W}.
Use reflexivity.
rewrite the current goal using HdefCylW (from left to right).
We prove the intermediate claim HpropW: i ∈ I ∧ W ∈ space_family_topology Xi i ∧ apply_fun f i ∈ W.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HiI.
An exact proof term for the current goal is HW0.
An exact proof term for the current goal is HfiW.
An exact proof term for the current goal is (SepI X (λg : set ⇒ i ∈ I ∧ W ∈ space_family_topology Xi i ∧ apply_fun g i ∈ W) f HfX HpropW).
We prove the intermediate claim Hcliff_prod: f ∈ closure_of X T (product_cylinder I Xi i V) ↔ (∀O ∈ T, f ∈ O → O ∩ product_cylinder I Xi i V ≠ Empty).
An exact proof term for the current goal is (closure_characterization X T (product_cylinder I Xi i V) f HT HfX).
We prove the intermediate claim HallO: ∀O ∈ T, f ∈ O → O ∩ product_cylinder I Xi i V ≠ Empty.
An exact proof term for the current goal is (iffEL (f ∈ closure_of X T (product_cylinder I Xi i V)) (∀O ∈ T, f ∈ O → O ∩ product_cylinder I Xi i V ≠ Empty) Hcliff_prod Hfcl).
We prove the intermediate claim Hcontr: N ∩ product_cylinder I Xi i V ≠ Empty.
An exact proof term for the current goal is (HallO N HNopen HfN).
We prove the intermediate claim HNintEmpty: N ∩ product_cylinder I Xi i V = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ N ∩ product_cylinder I Xi i V.
We will prove z ∈ Empty.
We prove the intermediate claim HzN: z ∈ N.
An exact proof term for the current goal is (binintersectE1 N (product_cylinder I Xi i V) z Hz).
We prove the intermediate claim HzV: z ∈ product_cylinder I Xi i V.
An exact proof term for the current goal is (binintersectE2 N (product_cylinder I Xi i V) z Hz).
We prove the intermediate claim HzNprop: i ∈ I ∧ W ∈ space_family_topology Xi i ∧ apply_fun z i ∈ W.
An exact proof term for the current goal is (SepE2 X (λg : set ⇒ i ∈ I ∧ W ∈ space_family_topology Xi i ∧ apply_fun g i ∈ W) z HzN).
We prove the intermediate claim HzVprop: i ∈ I ∧ V ∈ space_family_topology Xi i ∧ apply_fun z i ∈ V.
An exact proof term for the current goal is (SepE2 X (λg : set ⇒ i ∈ I ∧ V ∈ space_family_topology Xi i ∧ apply_fun g i ∈ V) z HzV).
We prove the intermediate claim HziW: apply_fun z i ∈ W.
An exact proof term for the current goal is (andER (i ∈ I ∧ W ∈ space_family_topology Xi i) (apply_fun z i ∈ W) HzNprop).
We prove the intermediate claim HziV: apply_fun z i ∈ V.
An exact proof term for the current goal is (andER (i ∈ I ∧ V ∈ space_family_topology Xi i) (apply_fun z i ∈ V) HzVprop).
We prove the intermediate claim HziWV: apply_fun z i ∈ W ∩ V.
An exact proof term for the current goal is (binintersectI W V (apply_fun z i) HziW HziV).
We prove the intermediate claim HziE: apply_fun z i ∈ Empty.
rewrite the current goal using HWdisj (from right to left).
An exact proof term for the current goal is HziWV.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE (apply_fun z i) HziE).
An exact proof term for the current goal is (Hcontr HNintEmpty).
∎