We will prove topology_on (product_space I Xi) (product_topology_full I Xi) ∧ ∀x : set, x ∈ product_space I Xi → closed_in (product_space I Xi) (product_topology_full I Xi) {x}.

Apply andI to the current goal.

We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Hreg: regular_space (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (Hrfam i HiI).

We prove the intermediate claim Hopc: one_point_sets_closed (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (andEL (one_point_sets_closed (product_component Xi i) (product_component_topology Xi i)) (∀x : set, x ∈ product_component Xi i → ∀F : set, closed_in (product_component Xi i) (product_component_topology Xi i) F → x ∉ F → ∃U V : set, U ∈ product_component_topology Xi i ∧ V ∈ product_component_topology Xi i ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).

An exact proof term for the current goal is (andEL (topology_on (product_component Xi i) (product_component_topology Xi i)) (∀x : set, x ∈ product_component Xi i → closed_in (product_component Xi i) (product_component_topology Xi i) {x}) Hopc).

An exact proof term for the current goal is (product_topology_full_is_topology I Xi HcompTop).

Let x be given.

Assume Hx: x ∈ product_space I Xi.

We will prove closed_in (product_space I Xi) (product_topology_full I Xi) {x}.

Apply (xm (I = Empty)) to the current goal.

Assume HI0: I = Empty.

rewrite the current goal using HI0 (from left to right).

We prove the intermediate claim HX0: product_space Empty Xi = {Empty}.

An exact proof term for the current goal is (product_space_empty_index Xi).

We prove the intermediate claim HxEidx: x ∈ product_space Empty Xi.

We will prove x ∈ product_space Empty Xi.

rewrite the current goal using HI0 (from right to left).

An exact proof term for the current goal is Hx.

We prove the intermediate claim HxS: x ∈ {Empty}.

rewrite the current goal using HX0 (from right to left).

An exact proof term for the current goal is HxEidx.

We prove the intermediate claim HxEq: x = Empty.

An exact proof term for the current goal is (SingE Empty x HxS).

We prove the intermediate claim HT0: topology_on (product_space Empty Xi) (product_topology_full Empty Xi).

An exact proof term for the current goal is (product_topology_full_empty_is_topology Xi).

We prove the intermediate claim HsetEq: {x} = product_space Empty Xi.

rewrite the current goal using HxEq (from left to right).

rewrite the current goal using HX0 (from right to left).

Use reflexivity.

rewrite the current goal using HsetEq (from left to right).

An exact proof term for the current goal is (X_is_closed (product_space Empty Xi) (product_topology_full Empty Xi) HT0).

Assume HIne: I ≠ Empty.

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 prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Hreg: regular_space (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (Hrfam i HiI).

We prove the intermediate claim Hopc: one_point_sets_closed (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (andEL (one_point_sets_closed (product_component Xi i) (product_component_topology Xi i)) (∀x0 : set, x0 ∈ product_component Xi i → ∀F0 : set, closed_in (product_component Xi i) (product_component_topology Xi i) F0 → x0 ∉ F0 → ∃U0 V0 : set, U0 ∈ product_component_topology Xi i ∧ V0 ∈ product_component_topology Xi i ∧ x0 ∈ U0 ∧ F0 ⊆ V0 ∧ U0 ∩ V0 = Empty) Hreg).

An exact proof term for the current goal is (andEL (topology_on (product_component Xi i) (product_component_topology Xi i)) (∀x0 : set, x0 ∈ product_component Xi i → closed_in (product_component Xi i) (product_component_topology Xi i) {x0}) Hopc).

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).

Set Ofam to be the term {U ∈ T|x ∉ U}.

We prove the intermediate claim HOfamSub: Ofam ⊆ T.

Let U be given.

Assume HU: U ∈ Ofam.

An exact proof term for the current goal is (SepE1 T (λU0 : set ⇒ x ∉ U0) U HU).

We prove the intermediate claim HUnionOpen: ⋃ Ofam ∈ T.

An exact proof term for the current goal is (topology_union_closed X T Ofam HT HOfamSub).

We prove the intermediate claim HUnionEq: ⋃ Ofam = X ∖ {x}.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ ⋃ Ofam.

Apply UnionE_impred Ofam y Hy to the current goal.

Let U be given.

Assume HyU: y ∈ U.

Assume HUfam: U ∈ Ofam.

We prove the intermediate claim HUT: U ∈ T.

An exact proof term for the current goal is (SepE1 T (λU0 : set ⇒ x ∉ U0) U HUfam).

We prove the intermediate claim HxnotU: x ∉ U.

An exact proof term for the current goal is (SepE2 T (λU0 : set ⇒ x ∉ U0) U HUfam).

We prove the intermediate claim HUSubX: U ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X T U HT HUT).

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HUSubX y HyU).

We prove the intermediate claim HynotSing: y ∉ {x}.

Assume HySing: y ∈ {x}.

Apply FalseE to the current goal.

We prove the intermediate claim Hyeq: y = x.

An exact proof term for the current goal is (SingE x y HySing).

We prove the intermediate claim HxU: x ∈ U.

We will prove x ∈ U.

rewrite the current goal using Hyeq (from right to left).

An exact proof term for the current goal is HyU.

An exact proof term for the current goal is (HxnotU HxU).

Apply setminusI to the current goal.

An exact proof term for the current goal is HyX.

An exact proof term for the current goal is HynotSing.

Let y be given.

Assume Hy: y ∈ X ∖ {x}.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (setminusE1 X {x} y Hy).

We prove the intermediate claim HynotSing: y ∉ {x}.

An exact proof term for the current goal is (setminusE2 X {x} y Hy).

We prove the intermediate claim Hyneq: y ≠ x.

Assume Hyeq: y = x.

Apply FalseE to the current goal.

We prove the intermediate claim HySing: y ∈ {x}.

We will prove y ∈ {x}.

rewrite the current goal using Hyeq (from left to right).

An exact proof term for the current goal is (SingI x).

An exact proof term for the current goal is (HynotSing HySing).

We prove the intermediate claim Hexi: ∃i : set, i ∈ I ∧ apply_fun y i ≠ apply_fun x i.

An exact proof term for the current goal is (product_space_points_differ_coord I Xi y x HyX Hx Hyneq).

Apply Hexi to the current goal.

Let i be given.

Assume Hiconj.

We prove the intermediate claim HiI: i ∈ I.

An exact proof term for the current goal is (andEL (i ∈ I) (apply_fun y i ≠ apply_fun x i) Hiconj).

We prove the intermediate claim Hdiff: apply_fun y i ≠ apply_fun x i.

An exact proof term for the current goal is (andER (i ∈ I) (apply_fun y i ≠ apply_fun x i) Hiconj).

We prove the intermediate claim Hregi: regular_space (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (Hrfam i HiI).

We prove the intermediate claim Hopci: one_point_sets_closed (product_component Xi i) (product_component_topology Xi i).

We prove the intermediate claim HTi: topology_on (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (andEL (topology_on (product_component Xi i) (product_component_topology Xi i)) (∀z : set, z ∈ product_component Xi i → closed_in (product_component Xi i) (product_component_topology Xi i) {z}) Hopci).

We prove the intermediate claim Hxiprop: total_function_on x I (space_family_union I Xi) ∧ functional_graph x ∧ ∀j : set, j ∈ I → apply_fun x j ∈ space_family_set Xi j.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf : set ⇒ 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) x Hx).

We prove the intermediate claim Hxiall: ∀j : set, j ∈ I → apply_fun x j ∈ space_family_set Xi j.

An exact proof term for the current goal is (andER (total_function_on x I (space_family_union I Xi) ∧ functional_graph x) (∀j : set, j ∈ I → apply_fun x j ∈ space_family_set Xi j) Hxiprop).

We prove the intermediate claim Hxi: apply_fun x i ∈ product_component Xi i.

An exact proof term for the current goal is (Hxiall i HiI).

We prove the intermediate claim Hyprop: total_function_on y I (space_family_union I Xi) ∧ functional_graph y ∧ ∀j : set, j ∈ I → apply_fun y j ∈ space_family_set Xi j.

We prove the intermediate claim Hyall: ∀j : set, j ∈ I → apply_fun y j ∈ space_family_set Xi j.

An exact proof term for the current goal is (andER (total_function_on y I (space_family_union I Xi) ∧ functional_graph y) (∀j : set, j ∈ I → apply_fun y j ∈ space_family_set Xi j) Hyprop).

We prove the intermediate claim Hyi: apply_fun y i ∈ product_component Xi i.

An exact proof term for the current goal is (Hyall i HiI).

We prove the intermediate claim Hsingcl: closed_in (product_component Xi i) (product_component_topology Xi i) {apply_fun x i}.

An exact proof term for the current goal is (andER (topology_on (product_component Xi i) (product_component_topology Xi i)) (∀z : set, z ∈ product_component Xi i → closed_in (product_component Xi i) (product_component_topology Xi i) {z}) Hopci (apply_fun x i) Hxi).

We prove the intermediate claim Hpkg: {apply_fun x i} ⊆ product_component Xi i ∧ ∃U0 ∈ product_component_topology Xi i, {apply_fun x i} = (product_component Xi i) ∖ U0.

An exact proof term for the current goal is (closed_in_package (product_component Xi i) (product_component_topology Xi i) {apply_fun x i} Hsingcl).

We prove the intermediate claim HexU0: ∃U0 ∈ product_component_topology Xi i, {apply_fun x i} = (product_component Xi i) ∖ U0.

An exact proof term for the current goal is (andER ({apply_fun x i} ⊆ product_component Xi i) (∃U0 ∈ product_component_topology Xi i, {apply_fun x i} = (product_component Xi i) ∖ U0) Hpkg).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0conj.

We prove the intermediate claim HU0top: U0 ∈ product_component_topology Xi i.

An exact proof term for the current goal is (andEL (U0 ∈ product_component_topology Xi i) ({apply_fun x i} = product_component Xi i ∖ U0) HU0conj).

We prove the intermediate claim HsingEq: {apply_fun x i} = product_component Xi i ∖ U0.

An exact proof term for the current goal is (andER (U0 ∈ product_component_topology Xi i) ({apply_fun x i} = product_component Xi i ∖ U0) HU0conj).

We prove the intermediate claim Hxi_in_sing: apply_fun x i ∈ {apply_fun x i}.

An exact proof term for the current goal is (SingI (apply_fun x i)).

We prove the intermediate claim Hxi_in_comp: apply_fun x i ∈ product_component Xi i ∖ U0.

rewrite the current goal using HsingEq (from right to left).

An exact proof term for the current goal is Hxi_in_sing.

We prove the intermediate claim Hxi_notU0: apply_fun x i ∉ U0.

An exact proof term for the current goal is (setminusE2 (product_component Xi i) U0 (apply_fun x i) Hxi_in_comp).

We prove the intermediate claim Hyi_notSing: apply_fun y i ∉ {apply_fun x i}.

Assume HySing: apply_fun y i ∈ {apply_fun x i}.

Apply FalseE to the current goal.

We prove the intermediate claim Heq: apply_fun y i = apply_fun x i.

An exact proof term for the current goal is (SingE (apply_fun x i) (apply_fun y i) HySing).

An exact proof term for the current goal is (Hdiff Heq).

We prove the intermediate claim Hyi_inU0: apply_fun y i ∈ U0.

Apply (xm (apply_fun y i ∈ U0)) to the current goal.

Assume Hyes.

An exact proof term for the current goal is Hyes.

Assume HnoU: apply_fun y i ∉ U0.

Apply FalseE to the current goal.

We prove the intermediate claim Hyi_in_comp2: apply_fun y i ∈ product_component Xi i ∖ U0.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hyi.

An exact proof term for the current goal is HnoU.

We prove the intermediate claim Hyi_in_sing2: apply_fun y i ∈ {apply_fun x i}.

rewrite the current goal using HsingEq (from left to right).

An exact proof term for the current goal is Hyi_in_comp2.

An exact proof term for the current goal is (Hyi_notSing Hyi_in_sing2).

Set U to be the term product_cylinder I Xi i U0.

We prove the intermediate claim HUsub: U ∈ S.

We will prove U ∈ S.

We will prove U ∈ (⋃_{j ∈ I}{product_cylinder I Xi j W|W ∈ space_family_topology Xi j}).

Apply (famunionI I (λj : set ⇒ {product_cylinder I Xi j W|W ∈ space_family_topology Xi j}) i U HiI) to the current goal.

An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λW : set ⇒ product_cylinder I Xi i W) U0 HU0top).

We prove the intermediate claim HUopen: U ∈ T.

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X S U HSsub HUsub).

We prove the intermediate claim HyU: y ∈ U.

We prove the intermediate claim HdefU: U = {f ∈ X|i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0}.

Use reflexivity.

rewrite the current goal using HdefU (from left to right).

Apply (SepI X (λf : set ⇒ i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0) y HyX) 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 HU0top.

An exact proof term for the current goal is Hyi_inU0.

We prove the intermediate claim HxnotU: x ∉ U.

Assume HxU: x ∈ U.

We prove the intermediate claim HdefU: U = {f ∈ X|i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0}.

Use reflexivity.

We prove the intermediate claim HxU2: x ∈ {f ∈ X|i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0}.

rewrite the current goal using HdefU (from right to left).

An exact proof term for the current goal is HxU.

We prove the intermediate claim Hxprop2: i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun x i ∈ U0.

An exact proof term for the current goal is (SepE2 X (λf : set ⇒ i ∈ I ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0) x HxU2).

We prove the intermediate claim Hx_inU0: apply_fun x i ∈ U0.

An exact proof term for the current goal is (andER (i ∈ I ∧ U0 ∈ space_family_topology Xi i) (apply_fun x i ∈ U0) Hxprop2).

An exact proof term for the current goal is (Hxi_notU0 Hx_inU0).

We prove the intermediate claim HUfam: U ∈ Ofam.

Apply (SepI T (λU1 : set ⇒ x ∉ U1) U HUopen) to the current goal.

An exact proof term for the current goal is HxnotU.

An exact proof term for the current goal is (UnionI Ofam y U HyU HUfam).

We prove the intermediate claim HopenComp: X ∖ {x} ∈ T.

rewrite the current goal using HUnionEq (from right to left).

An exact proof term for the current goal is HUnionOpen.

We prove the intermediate claim HsingSub: {x} ⊆ X.

An exact proof term for the current goal is (singleton_subset x X Hx).

Apply (closed_inI X T {x} HT HsingSub) to the current goal.

We use (X ∖ {x}) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HopenComp.

We will prove {x} = X ∖ (X ∖ {x}).

rewrite the current goal using (setminus_setminus_eq X {x} HsingSub) (from left to right).

Use reflexivity.

Apply (xm (I = Empty)) to the current goal.

Assume HI0: I = Empty.

rewrite the current goal using HI0 (from left to right).

Let x be given.

Assume Hx: x ∈ product_space Empty Xi.

Let F be given.

Assume HF: closed_in (product_space Empty Xi) (product_topology_full Empty Xi) F.

Assume HxnotF: x ∉ F.

We will prove ∃U V : set, U ∈ product_topology_full Empty Xi ∧ V ∈ product_topology_full Empty Xi ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.

We prove the intermediate claim HT0: topology_on (product_space Empty Xi) (product_topology_full Empty Xi).

An exact proof term for the current goal is (product_topology_full_empty_is_topology Xi).

We use (product_space Empty Xi) to witness the existential quantifier.

We use Empty to witness the existential quantifier.

Apply and5I to the current goal.

An exact proof term for the current goal is (topology_has_X (product_space Empty Xi) (product_topology_full Empty Xi) HT0).

An exact proof term for the current goal is (topology_has_empty (product_space Empty Xi) (product_topology_full Empty Xi) HT0).

An exact proof term for the current goal is Hx.

Let y be given.

Assume HyF: y ∈ F.

We will prove y ∈ Empty.

We prove the intermediate claim HFsub: F ⊆ product_space Empty Xi.

An exact proof term for the current goal is (closed_in_subset (product_space Empty Xi) (product_topology_full Empty Xi) F HF).

We prove the intermediate claim HyX: y ∈ product_space Empty Xi.

An exact proof term for the current goal is (HFsub y HyF).

We prove the intermediate claim HX0: product_space Empty Xi = {Empty}.

An exact proof term for the current goal is (product_space_empty_index Xi).

We prove the intermediate claim HyS: y ∈ {Empty}.

rewrite the current goal using HX0 (from right to left).

An exact proof term for the current goal is HyX.

We prove the intermediate claim HyEq: y = Empty.

An exact proof term for the current goal is (SingE Empty y HyS).

We prove the intermediate claim HxS: x ∈ {Empty}.

rewrite the current goal using HX0 (from right to left).

An exact proof term for the current goal is Hx.

We prove the intermediate claim HxEq: x = Empty.

An exact proof term for the current goal is (SingE Empty x HxS).

We prove the intermediate claim Hyx: y = x.

rewrite the current goal using HyEq (from left to right).

rewrite the current goal using HxEq (from right to left).

Use reflexivity.

Apply FalseE to the current goal.

We prove the intermediate claim HxF: x ∈ F.

We will prove x ∈ F.

rewrite the current goal using Hyx (from right to left).

An exact proof term for the current goal is HyF.

An exact proof term for the current goal is (HxnotF HxF).

We prove the intermediate claim Hinter: (product_space Empty Xi) ∩ Empty = Empty.

An exact proof term for the current goal is (binintersect_Empty_right (product_space Empty Xi)).

An exact proof term for the current goal is Hinter.

Assume HIne: I ≠ Empty.

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 prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Hreg: regular_space (product_component Xi i) (product_component_topology Xi i).

An exact proof term for the current goal is (Hrfam i HiI).

We prove the intermediate claim Hopc: one_point_sets_closed (product_component Xi i) (product_component_topology Xi i).

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 x be given.

Assume Hx: x ∈ X.

Let F be given.

Assume HF: closed_in X T F.

Assume HxnotF: x ∉ F.

We will prove ∃U V : set, U ∈ T ∧ V ∈ T ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.

Apply (xm (F = Empty)) to the current goal.

Assume HF0: F = Empty.

We use X to witness the existential quantifier.

We use Empty to witness the existential quantifier.

Apply and5I to the current goal.

An exact proof term for the current goal is (topology_has_X X T HT).

An exact proof term for the current goal is (topology_has_empty X T HT).

An exact proof term for the current goal is Hx.

Let y be given.

Assume HyF: y ∈ F.

We will prove y ∈ Empty.

rewrite the current goal using HF0 (from right to left).

An exact proof term for the current goal is HyF.

We prove the intermediate claim Hinter: X ∩ Empty = Empty.

An exact proof term for the current goal is (binintersect_Empty_right X).

An exact proof term for the current goal is Hinter.

Assume HFne: F ≠ Empty.

We prove the intermediate claim HFpkg: F ⊆ X ∧ ∃Uc ∈ T, F = X ∖ Uc.

An exact proof term for the current goal is (closed_in_package X T F HF).

We prove the intermediate claim HFsubX: F ⊆ X.

An exact proof term for the current goal is (andEL (F ⊆ X) (∃Uc ∈ T, F = X ∖ Uc) HFpkg).

We prove the intermediate claim HexUc: ∃Uc ∈ T, F = X ∖ Uc.

An exact proof term for the current goal is (andER (F ⊆ X) (∃Uc ∈ T, F = X ∖ Uc) HFpkg).

Apply HexUc to the current goal.

Let Uc be given.

Assume HUc_conj.

Apply HUc_conj to the current goal.

Assume HUcT: Uc ∈ T.

Assume HFeq: F = X ∖ Uc.

We prove the intermediate claim HxUc: x ∈ Uc.

Apply (xm (x ∈ Uc)) to the current goal.

Assume H.

An exact proof term for the current goal is H.

Assume HxnotUc: x ∉ Uc.

Apply FalseE to the current goal.

We prove the intermediate claim HxF: x ∈ F.

rewrite the current goal using HFeq (from left to right).

An exact proof term for the current goal is (setminusI X Uc x Hx HxnotUc).

An exact proof term for the current goal is (HxnotF HxF).

We prove the intermediate claim HTdef1: T = generated_topology_from_subbasis X S.

Use reflexivity.

We prove the intermediate claim HTdef2: generated_topology_from_subbasis X S = generated_topology X (basis_of_subbasis X S).

Use reflexivity.

We prove the intermediate claim HUcG: Uc ∈ generated_topology X (basis_of_subbasis X S).

rewrite the current goal using HTdef2 (from right to left).

rewrite the current goal using HTdef1 (from right to left).

An exact proof term for the current goal is HUcT.

We prove the intermediate claim HUc_local: ∀z ∈ Uc, ∃b ∈ basis_of_subbasis X S, z ∈ b ∧ b ⊆ Uc.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ basis_of_subbasis X S, z ∈ b ∧ b ⊆ U0) Uc HUcG).

We prove the intermediate claim Hexb0: ∃b0 ∈ basis_of_subbasis X S, x ∈ b0 ∧ b0 ⊆ Uc.

An exact proof term for the current goal is (HUc_local x HxUc).

Apply Hexb0 to the current goal.

Let b0 be given.

Assume Hb0_conj.

Apply Hb0_conj to the current goal.

Assume Hb0B: b0 ∈ basis_of_subbasis X S.

Assume Hb0props.

We prove the intermediate claim Hxb0: x ∈ b0.

An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ Uc) Hb0props).

We prove the intermediate claim Hb0subUc: b0 ⊆ Uc.

An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ Uc) Hb0props).

We prove the intermediate claim HBasis: basis_on X (basis_of_subbasis X S).

An exact proof term for the current goal is (finite_intersections_basis_of_subbasis X S HSsub).

We prove the intermediate claim Hb0T: b0 ∈ T.

rewrite the current goal using HTdef1 (from left to right).

rewrite the current goal using HTdef2 (from left to right).

An exact proof term for the current goal is (generated_topology_contains_basis X (basis_of_subbasis X S) HBasis b0 Hb0B).

We prove the intermediate claim HexU: ∃U : set, U ∈ T ∧ x ∈ U ∧ U ⊆ b0 ∧ closure_of X T U ⊆ b0.

Apply (xm (b0 = X)) to the current goal.

Assume Hb0X: b0 = X.

We use X to witness the existential quantifier.

Apply and4I to the current goal.

An exact proof term for the current goal is (topology_has_X X T HT).

An exact proof term for the current goal is Hx.

rewrite the current goal using Hb0X (from left to right).

An exact proof term for the current goal is (Subq_ref X).

rewrite the current goal using Hb0X (from left to right).

We prove the intermediate claim HclXeq: closure_of X T X = X.

An exact proof term for the current goal is (closure_of_space X T HT).

rewrite the current goal using HclXeq (from left to right).

An exact proof term for the current goal is (Subq_ref X).

Assume Hb0neX: b0 ≠ X.

We prove the intermediate claim Hb0fin: b0 ∈ finite_intersections_of X S.

An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb : set ⇒ b ≠ Empty) b0 Hb0B).

We prove the intermediate claim Hb0ne: b0 ≠ Empty.

An exact proof term for the current goal is (SepE2 (finite_intersections_of X S) (λb : set ⇒ b ≠ Empty) b0 Hb0B).

We prove the intermediate claim HexF: ∃F ∈ finite_subcollections S, b0 = intersection_of_family X F.

An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF0 : set ⇒ intersection_of_family X F0) b0 Hb0fin).

Set F to be the term Eps_i (λF0 : set ⇒ F0 ∈ finite_subcollections S ∧ b0 = intersection_of_family X F0).

We prove the intermediate claim HFprop: F ∈ finite_subcollections S ∧ b0 = intersection_of_family X F.

An exact proof term for the current goal is (Eps_i_ex (λF0 : set ⇒ F0 ∈ finite_subcollections S ∧ b0 = intersection_of_family X F0) HexF).

We prove the intermediate claim HFfin: F ∈ finite_subcollections S.

An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S) (b0 = intersection_of_family X F) HFprop).

We prove the intermediate claim Hb0eqF: b0 = intersection_of_family X F.

An exact proof term for the current goal is (andER (F ∈ finite_subcollections S) (b0 = intersection_of_family X F) HFprop).

We prove the intermediate claim HxInInter: x ∈ intersection_of_family X F.

rewrite the current goal using Hb0eqF (from right to left).

An exact proof term for the current goal is Hxb0.

We prove the intermediate claim HxAll: ∀s : set, s ∈ F → x ∈ s.

An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ ∀U0 : set, U0 ∈ F → z0 ∈ U0) x HxInInter).

We prove the intermediate claim HFpowS: F ∈ 𝒫 S.

An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F HFfin).

We prove the intermediate claim HFin: finite F.

An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F HFfin).

We prove the intermediate claim HFsubS: F ⊆ S.

An exact proof term for the current goal is (PowerE S F HFpowS).

Set p to be the term λH : set ⇒ H ⊆ F → ∃U0 : set, U0 ∈ T ∧ x ∈ U0 ∧ U0 ⊆ intersection_of_family X H ∧ closure_of X T U0 ⊆ intersection_of_family X H of type set → prop.

We prove the intermediate claim HpEmpty: p Empty.

Assume Hsub: Empty ⊆ F.

We use X to witness the existential quantifier.

Apply and4I to the current goal.

An exact proof term for the current goal is (topology_has_X X T HT).

An exact proof term for the current goal is Hx.

rewrite the current goal using (intersection_of_family_empty_eq X) (from left to right).

An exact proof term for the current goal is (Subq_ref X).

rewrite the current goal using (intersection_of_family_empty_eq X) (from left to right).

We prove the intermediate claim HclX: closure_of X T X = X.

An exact proof term for the current goal is (closure_of_space X T HT).

rewrite the current goal using HclX (from left to right).

An exact proof term for the current goal is (Subq_ref X).

We prove the intermediate claim HpStep: ∀H y : set, finite H → y ∉ H → p H → p (H ∪ {y}).

Let H and y be given.

Assume HfH: finite H.

Assume HyNotH: y ∉ H.

Assume HpH: p H.

We will prove p (H ∪ {y}).

Assume HsubHF: (H ∪ {y}) ⊆ F.

We prove the intermediate claim HsubH: H ⊆ H ∪ {y}.

An exact proof term for the current goal is (binunion_Subq_1 H {y}).

We prove the intermediate claim HsubF: H ⊆ F.

An exact proof term for the current goal is (Subq_tra H (H ∪ {y}) F HsubH HsubHF).

We prove the intermediate claim HyIn: y ∈ H ∪ {y}.

An exact proof term for the current goal is (binunionI2 H {y} y (SingI y)).

We prove the intermediate claim HyF: y ∈ F.

An exact proof term for the current goal is (HsubHF y HyIn).

We prove the intermediate claim HexUh: ∃Uh : set, Uh ∈ T ∧ x ∈ Uh ∧ Uh ⊆ intersection_of_family X H ∧ closure_of X T Uh ⊆ intersection_of_family X H.

An exact proof term for the current goal is (HpH HsubF).

Apply HexUh to the current goal.

Let Uh be given.

Assume HUh_conj.

We prove the intermediate claim HUh12: (Uh ∈ T ∧ x ∈ Uh ∧ Uh ⊆ intersection_of_family X H).

An exact proof term for the current goal is (andEL (Uh ∈ T ∧ x ∈ Uh ∧ Uh ⊆ intersection_of_family X H) (closure_of X T Uh ⊆ intersection_of_family X H) HUh_conj).

We prove the intermediate claim HclUh: closure_of X T Uh ⊆ intersection_of_family X H.

An exact proof term for the current goal is (andER (Uh ∈ T ∧ x ∈ Uh ∧ Uh ⊆ intersection_of_family X H) (closure_of X T Uh ⊆ intersection_of_family X H) HUh_conj).

We prove the intermediate claim HUhTxHx: Uh ∈ T ∧ x ∈ Uh.

An exact proof term for the current goal is (andEL (Uh ∈ T ∧ x ∈ Uh) (Uh ⊆ intersection_of_family X H) HUh12).

We prove the intermediate claim HUhT: Uh ∈ T.

An exact proof term for the current goal is (andEL (Uh ∈ T) (x ∈ Uh) HUhTxHx).

We prove the intermediate claim HxUh: x ∈ Uh.

An exact proof term for the current goal is (andER (Uh ∈ T) (x ∈ Uh) HUhTxHx).

We prove the intermediate claim HUhsub: Uh ⊆ intersection_of_family X H.

An exact proof term for the current goal is (andER (Uh ∈ T ∧ x ∈ Uh) (Uh ⊆ intersection_of_family X H) HUh12).

We prove the intermediate claim HyS: y ∈ S.

An exact proof term for the current goal is (HFsubS y HyF).

Set Fam to be the term (λi0 : set ⇒ {product_cylinder I Xi i0 U0|U0 ∈ space_family_topology Xi i0}).

We prove the intermediate claim HSdef: S = (⋃_{i0 ∈ I}Fam i0).

Use reflexivity.

We prove the intermediate claim HyFam: y ∈ (⋃_{i0 ∈ I}Fam i0).

rewrite the current goal using HSdef (from right to left).

An exact proof term for the current goal is HyS.

We prove the intermediate claim HexiU: ∃i0 : set, i0 ∈ I ∧ ∃U0 ∈ space_family_topology Xi i0, y = product_cylinder I Xi i0 U0.

Apply (famunionE_impred I Fam y HyFam (∃i0 : set, i0 ∈ I ∧ ∃U0 ∈ space_family_topology Xi i0, y = product_cylinder I Xi i0 U0)) to the current goal.

Let i0 be given.

Assume Hi0I: i0 ∈ I.

Assume HyFi0: y ∈ Fam i0.

We prove the intermediate claim HexU0: ∃U0 ∈ space_family_topology Xi i0, y = product_cylinder I Xi i0 U0.

An exact proof term for the current goal is (ReplE (space_family_topology Xi i0) (λU0 : set ⇒ product_cylinder I Xi i0 U0) y HyFi0).

We use i0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hi0I.

An exact proof term for the current goal is HexU0.

Apply HexiU to the current goal.

Let i0 be given.

Assume Hi0conj.

We prove the intermediate claim Hi0I: i0 ∈ I.

An exact proof term for the current goal is (andEL (i0 ∈ I) (∃U0 ∈ space_family_topology Xi i0, y = product_cylinder I Xi i0 U0) Hi0conj).

We prove the intermediate claim HexU0: ∃U0 ∈ space_family_topology Xi i0, y = product_cylinder I Xi i0 U0.

An exact proof term for the current goal is (andER (i0 ∈ I) (∃U0 ∈ space_family_topology Xi i0, y = product_cylinder I Xi i0 U0) Hi0conj).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0conj.

We prove the intermediate claim HU0top: U0 ∈ space_family_topology Xi i0.

An exact proof term for the current goal is (andEL (U0 ∈ space_family_topology Xi i0) (y = product_cylinder I Xi i0 U0) HU0conj).

We prove the intermediate claim HyEq: y = product_cylinder I Xi i0 U0.

An exact proof term for the current goal is (andER (U0 ∈ space_family_topology Xi i0) (y = product_cylinder I Xi i0 U0) HU0conj).

We prove the intermediate claim Hxy: x ∈ y.

An exact proof term for the current goal is (HxAll y HyF).

We prove the intermediate claim HxCyl: x ∈ product_cylinder I Xi i0 U0.

rewrite the current goal using HyEq (from right to left).

An exact proof term for the current goal is Hxy.

We prove the intermediate claim HxCylProp: i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun x i0 ∈ U0.

An exact proof term for the current goal is (SepE2 X (λf0 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f0 i0 ∈ U0) x HxCyl).

We prove the intermediate claim Hxi0U0: apply_fun x i0 ∈ U0.

An exact proof term for the current goal is (andER (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) (apply_fun x i0 ∈ U0) HxCylProp).

We prove the intermediate claim Hreg0: regular_space (product_component Xi i0) (product_component_topology Xi i0).

An exact proof term for the current goal is (Hrfam i0 Hi0I).

We prove the intermediate claim Hregi0: regular_space (space_family_set Xi i0) (space_family_topology Xi i0).

We prove the intermediate claim HeqX0: product_component Xi i0 = space_family_set Xi i0.

Use reflexivity.

We prove the intermediate claim HeqT0: product_component_topology Xi i0 = space_family_topology Xi i0.

Use reflexivity.

rewrite the current goal using HeqX0 (from right to left).

rewrite the current goal using HeqT0 (from right to left).

An exact proof term for the current goal is Hreg0.

We prove the intermediate claim Hxprop: total_function_on x I (space_family_union I Xi) ∧ functional_graph x ∧ ∀j : set, j ∈ I → apply_fun x j ∈ space_family_set Xi j.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀j : set, j ∈ I → apply_fun f0 j ∈ space_family_set Xi j) x Hx).

We prove the intermediate claim HcoordsX: ∀j : set, j ∈ I → apply_fun x j ∈ space_family_set Xi j.

An exact proof term for the current goal is (andER (total_function_on x I (space_family_union I Xi) ∧ functional_graph x) (∀j : set, j ∈ I → apply_fun x j ∈ space_family_set Xi j) Hxprop).

We prove the intermediate claim Hxi0X0: apply_fun x i0 ∈ space_family_set Xi i0.

An exact proof term for the current goal is (HcoordsX i0 Hi0I).

We prove the intermediate claim HexV0: ∃V0 : set, V0 ∈ space_family_topology Xi i0 ∧ apply_fun x i0 ∈ V0 ∧ closure_of (space_family_set Xi i0) (space_family_topology Xi i0) V0 ⊆ U0.

An exact proof term for the current goal is (regular_space_shrink_neighborhood (space_family_set Xi i0) (space_family_topology Xi i0) (apply_fun x i0) U0 Hregi0 Hxi0X0 HU0top Hxi0U0).

Apply HexV0 to the current goal.

Let V0 be given.

Assume HV0conj.

We prove the intermediate claim HV0core: V0 ∈ space_family_topology Xi i0 ∧ apply_fun x i0 ∈ V0.

An exact proof term for the current goal is (andEL (V0 ∈ space_family_topology Xi i0 ∧ apply_fun x i0 ∈ V0) (closure_of (space_family_set Xi i0) (space_family_topology Xi i0) V0 ⊆ U0) HV0conj).

We prove the intermediate claim HV0top: V0 ∈ space_family_topology Xi i0.

An exact proof term for the current goal is (andEL (V0 ∈ space_family_topology Xi i0) (apply_fun x i0 ∈ V0) HV0core).

We prove the intermediate claim Hxi0V0: apply_fun x i0 ∈ V0.

An exact proof term for the current goal is (andER (V0 ∈ space_family_topology Xi i0) (apply_fun x i0 ∈ V0) HV0core).

We prove the intermediate claim HclV0subU0: closure_of (space_family_set Xi i0) (space_family_topology Xi i0) V0 ⊆ U0.

An exact proof term for the current goal is (andER (V0 ∈ space_family_topology Xi i0 ∧ apply_fun x i0 ∈ V0) (closure_of (space_family_set Xi i0) (space_family_topology Xi i0) V0 ⊆ U0) HV0conj).

We prove the intermediate claim Htopi: topology_on (space_family_set Xi i0) (space_family_topology Xi i0).

An exact proof term for the current goal is (HcompTop i0 Hi0I).

We prove the intermediate claim HTsubXi: space_family_topology Xi i0 ⊆ 𝒫 (space_family_set Xi i0).

An exact proof term for the current goal is (topology_subset_axiom (space_family_set Xi i0) (space_family_topology Xi i0) Htopi).

We prove the intermediate claim HV0subXi: V0 ⊆ space_family_set Xi i0.

An exact proof term for the current goal is (PowerE (space_family_set Xi i0) V0 (HTsubXi V0 HV0top)).

We prove the intermediate claim HV0subCl: V0 ⊆ closure_of (space_family_set Xi i0) (space_family_topology Xi i0) V0.

An exact proof term for the current goal is (subset_of_closure (space_family_set Xi i0) (space_family_topology Xi i0) V0 Htopi HV0subXi).

We prove the intermediate claim HV0subU0: V0 ⊆ U0.

An exact proof term for the current goal is (Subq_tra V0 (closure_of (space_family_set Xi i0) (space_family_topology Xi i0) V0) U0 HV0subCl HclV0subU0).

Set Wcyl to be the term product_cylinder I Xi i0 V0.

We prove the intermediate claim HWcylS: Wcyl ∈ S.

We prove the intermediate claim HSdef2: S = (⋃_{j ∈ I}{product_cylinder I Xi j U1|U1 ∈ space_family_topology Xi j}).

Use reflexivity.

rewrite the current goal using HSdef2 (from left to right).

Apply (famunionI I (λj : set ⇒ {product_cylinder I Xi j U1|U1 ∈ space_family_topology Xi j}) i0 Wcyl Hi0I) to the current goal.

An exact proof term for the current goal is (ReplI (space_family_topology Xi i0) (λU1 : set ⇒ product_cylinder I Xi i0 U1) V0 HV0top).

We prove the intermediate claim HWcylT: Wcyl ∈ T.

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X S Wcyl HSsub HWcylS).

We prove the intermediate claim HxWcyl: x ∈ Wcyl.

We prove the intermediate claim HdefW: Wcyl = {f0 ∈ X|i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f0 i0 ∈ V0}.

Use reflexivity.

rewrite the current goal using HdefW (from left to right).

We prove the intermediate claim HpropW: i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun x i0 ∈ V0.

Apply andI to the current goal.

An exact proof term for the current goal is Hi0I.

An exact proof term for the current goal is HV0top.

An exact proof term for the current goal is Hxi0V0.

An exact proof term for the current goal is (SepI X (λf0 : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f0 i0 ∈ V0) x Hx HpropW).

We prove the intermediate claim HWsub: Wcyl ⊆ y.

rewrite the current goal using HyEq (from left to right).

Let f0 be given.

Assume Hf0: f0 ∈ Wcyl.

We will prove f0 ∈ product_cylinder I Xi i0 U0.

We prove the intermediate claim Hf0X: f0 ∈ X.

An exact proof term for the current goal is (SepE1 X (λg : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun g i0 ∈ V0) f0 Hf0).

We prove the intermediate claim Hprop0: i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f0 i0 ∈ V0.

An exact proof term for the current goal is (SepE2 X (λg : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun g i0 ∈ V0) f0 Hf0).

We prove the intermediate claim HfiV0: apply_fun f0 i0 ∈ V0.

An exact proof term for the current goal is (andER (i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0) (apply_fun f0 i0 ∈ V0) Hprop0).

We prove the intermediate claim HfiU0: apply_fun f0 i0 ∈ U0.

An exact proof term for the current goal is (HV0subU0 (apply_fun f0 i0) HfiV0).

We prove the intermediate claim HdefCylU0: product_cylinder I Xi i0 U0 = {g ∈ X|i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun g i0 ∈ U0}.

Use reflexivity.

rewrite the current goal using HdefCylU0 (from left to right).

We prove the intermediate claim HpropU0: i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f0 i0 ∈ U0.

Apply andI to the current goal.

An exact proof term for the current goal is Hi0I.

An exact proof term for the current goal is HU0top.

An exact proof term for the current goal is HfiU0.

An exact proof term for the current goal is (SepI X (λg : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun g i0 ∈ U0) f0 Hf0X HpropU0).

We prove the intermediate claim HclWsub: closure_of X T Wcyl ⊆ y.

rewrite the current goal using HyEq (from left to right).

An exact proof term for the current goal is (closure_of_product_cylinder_sub I Xi i0 V0 U0 HIne HcompTop Hi0I HV0top HU0top HclV0subU0).

Set Unew to be the term Uh ∩ Wcyl.

We prove the intermediate claim HUnewT: Unew ∈ T.

An exact proof term for the current goal is (lemma_intersection_two_open X T Uh Wcyl HT HUhT HWcylT).

We prove the intermediate claim HxUnew: x ∈ Unew.

An exact proof term for the current goal is (binintersectI Uh Wcyl x HxUh HxWcyl).

We prove the intermediate claim HinterEq: intersection_of_family X (H ∪ {y}) = (intersection_of_family X H) ∩ y.

An exact proof term for the current goal is (intersection_of_family_adjoin X H y).

We prove the intermediate claim HUnewSub: Unew ⊆ intersection_of_family X (H ∪ {y}).

rewrite the current goal using HinterEq (from left to right).

Let z be given.

Assume HzU: z ∈ Unew.

We will prove z ∈ (intersection_of_family X H) ∩ y.

We prove the intermediate claim HzUh: z ∈ Uh.

An exact proof term for the current goal is (binintersectE1 Uh Wcyl z HzU).

We prove the intermediate claim HzW: z ∈ Wcyl.

An exact proof term for the current goal is (binintersectE2 Uh Wcyl z HzU).

We prove the intermediate claim HzInterH: z ∈ intersection_of_family X H.

An exact proof term for the current goal is (HUhsub z HzUh).

We prove the intermediate claim Hzy: z ∈ y.

An exact proof term for the current goal is (HWsub z HzW).

An exact proof term for the current goal is (binintersectI (intersection_of_family X H) y z HzInterH Hzy).

We prove the intermediate claim HclUnewSub: closure_of X T Unew ⊆ intersection_of_family X (H ∪ {y}).

We prove the intermediate claim HTsubX: T ⊆ 𝒫 X.

An exact proof term for the current goal is (topology_subset_axiom X T HT).

We prove the intermediate claim HUhSubX: Uh ⊆ X.

An exact proof term for the current goal is (PowerE X Uh (HTsubX Uh HUhT)).

We prove the intermediate claim HWSubX: Wcyl ⊆ X.

An exact proof term for the current goal is (PowerE X Wcyl (HTsubX Wcyl HWcylT)).

We prove the intermediate claim HclInt: closure_of X T Unew ⊆ (closure_of X T Uh) ∩ (closure_of X T Wcyl).

An exact proof term for the current goal is (closure_intersection_contained X T Uh Wcyl HT HUhSubX HWSubX).

rewrite the current goal using HinterEq (from left to right).

Let z be given.

Assume Hzcl: z ∈ closure_of X T Unew.

We will prove z ∈ (intersection_of_family X H) ∩ y.

We prove the intermediate claim Hzcl2: z ∈ (closure_of X T Uh) ∩ (closure_of X T Wcyl).

An exact proof term for the current goal is (HclInt z Hzcl).

We prove the intermediate claim HzclUh: z ∈ closure_of X T Uh.

An exact proof term for the current goal is (binintersectE1 (closure_of X T Uh) (closure_of X T Wcyl) z Hzcl2).

We prove the intermediate claim HzclW: z ∈ closure_of X T Wcyl.

An exact proof term for the current goal is (binintersectE2 (closure_of X T Uh) (closure_of X T Wcyl) z Hzcl2).

We prove the intermediate claim HzInterH: z ∈ intersection_of_family X H.

An exact proof term for the current goal is (HclUh z HzclUh).

We prove the intermediate claim Hzy: z ∈ y.

An exact proof term for the current goal is (HclWsub z HzclW).

An exact proof term for the current goal is (binintersectI (intersection_of_family X H) y z HzInterH Hzy).

We use Unew to witness the existential quantifier.

Apply and4I to the current goal.

An exact proof term for the current goal is HUnewT.

An exact proof term for the current goal is HxUnew.

An exact proof term for the current goal is HUnewSub.

An exact proof term for the current goal is HclUnewSub.

We prove the intermediate claim HpAll: ∀H : set, finite H → p H.

An exact proof term for the current goal is (finite_ind p HpEmpty HpStep).

We prove the intermediate claim HpF: p F.

An exact proof term for the current goal is (HpAll F HFin).

We prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ T ∧ x ∈ U0 ∧ U0 ⊆ intersection_of_family X F ∧ closure_of X T U0 ⊆ intersection_of_family X F.

An exact proof term for the current goal is (HpF (Subq_ref F)).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0conj.

We prove the intermediate claim HU0l: (U0 ∈ T ∧ x ∈ U0 ∧ U0 ⊆ intersection_of_family X F).

An exact proof term for the current goal is (andEL (U0 ∈ T ∧ x ∈ U0 ∧ U0 ⊆ intersection_of_family X F) (closure_of X T U0 ⊆ intersection_of_family X F) HU0conj).

We prove the intermediate claim HU0cl: closure_of X T U0 ⊆ intersection_of_family X F.

An exact proof term for the current goal is (andER (U0 ∈ T ∧ x ∈ U0 ∧ U0 ⊆ intersection_of_family X F) (closure_of X T U0 ⊆ intersection_of_family X F) HU0conj).

We prove the intermediate claim HU0Tx: U0 ∈ T ∧ x ∈ U0.

An exact proof term for the current goal is (andEL (U0 ∈ T ∧ x ∈ U0) (U0 ⊆ intersection_of_family X F) HU0l).

We prove the intermediate claim HU0T: U0 ∈ T.

An exact proof term for the current goal is (andEL (U0 ∈ T) (x ∈ U0) HU0Tx).

We prove the intermediate claim HxU0: x ∈ U0.

An exact proof term for the current goal is (andER (U0 ∈ T) (x ∈ U0) HU0Tx).

We prove the intermediate claim HU0sub: U0 ⊆ intersection_of_family X F.

An exact proof term for the current goal is (andER (U0 ∈ T ∧ x ∈ U0) (U0 ⊆ intersection_of_family X F) HU0l).

We use U0 to witness the existential quantifier.

Apply and4I to the current goal.

An exact proof term for the current goal is HU0T.

An exact proof term for the current goal is HxU0.

rewrite the current goal using Hb0eqF (from left to right).

An exact proof term for the current goal is HU0sub.

rewrite the current goal using Hb0eqF (from left to right).

An exact proof term for the current goal is HU0cl.

Apply HexU to the current goal.

Let U be given.

Assume HU_conj.

We prove the intermediate claim HU12: (U ∈ T ∧ x ∈ U) ∧ U ⊆ b0.

An exact proof term for the current goal is (andEL ((U ∈ T ∧ x ∈ U) ∧ U ⊆ b0) (closure_of X T U ⊆ b0) HU_conj).

We prove the intermediate claim HclU_sub_b0: closure_of X T U ⊆ b0.

An exact proof term for the current goal is (andER ((U ∈ T ∧ x ∈ U) ∧ U ⊆ b0) (closure_of X T U ⊆ b0) HU_conj).

We prove the intermediate claim HU1: U ∈ T ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ T ∧ x ∈ U) (U ⊆ b0) HU12).

We prove the intermediate claim HUsubb0: U ⊆ b0.

An exact proof term for the current goal is (andER (U ∈ T ∧ x ∈ U) (U ⊆ b0) HU12).

We prove the intermediate claim HUinT: U ∈ T.

An exact proof term for the current goal is (andEL (U ∈ T) (x ∈ U) HU1).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ T) (x ∈ U) HU1).

We prove the intermediate claim HUsubX: U ⊆ X.

Let z be given.

Assume Hz: z ∈ U.

We will prove z ∈ X.

We prove the intermediate claim Hzb0: z ∈ b0.

An exact proof term for the current goal is (HUsubb0 z Hz).

We prove the intermediate claim HzUc: z ∈ Uc.

An exact proof term for the current goal is (Hb0subUc z Hzb0).

We prove the intermediate claim HUcsub: Uc ⊆ X.

We prove the intermediate claim HUcPow: Uc ∈ 𝒫 X.

An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ basis_of_subbasis X S, z ∈ b ∧ b ⊆ U0) Uc HUcG).

An exact proof term for the current goal is (PowerE X Uc HUcPow).

An exact proof term for the current goal is (HUcsub z HzUc).

We prove the intermediate claim HclU_sub_Uc: closure_of X T U ⊆ Uc.

Let y be given.

Assume HyCl: y ∈ closure_of X T U.

We will prove y ∈ Uc.

We prove the intermediate claim Hyb0: y ∈ b0.

An exact proof term for the current goal is (HclU_sub_b0 y HyCl).

An exact proof term for the current goal is (Hb0subUc y Hyb0).

We prove the intermediate claim HclU_closed: closed_in X T (closure_of X T U).

An exact proof term for the current goal is (closure_is_closed X T U HT HUsubX).

We prove the intermediate claim HclU_pkg: closure_of X T U ⊆ X ∧ ∃V0 ∈ T, closure_of X T U = X ∖ V0.

An exact proof term for the current goal is (closed_in_package X T (closure_of X T U) HclU_closed).

We prove the intermediate claim HexV0: ∃V0 ∈ T, closure_of X T U = X ∖ V0.

An exact proof term for the current goal is (andER (closure_of X T U ⊆ X) (∃V0 ∈ T, closure_of X T U = X ∖ V0) HclU_pkg).

Apply HexV0 to the current goal.

Let V0 be given.

Assume HV0_conj.

Apply HV0_conj to the current goal.

Assume HV0T: V0 ∈ T.

Assume HclEq: closure_of X T U = X ∖ V0.

We use U to witness the existential quantifier.

We use V0 to witness the existential quantifier.

Apply and5I to the current goal.

An exact proof term for the current goal is HUinT.

An exact proof term for the current goal is HV0T.

An exact proof term for the current goal is HxU.

Let y be given.

Assume HyF: y ∈ F.

We will prove y ∈ V0.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HFsubX y HyF).

We prove the intermediate claim HyNotUc: y ∉ Uc.

We prove the intermediate claim HyInXU: y ∈ X ∖ Uc.

rewrite the current goal using HFeq (from right to left).

An exact proof term for the current goal is HyF.

An exact proof term for the current goal is (setminusE2 X Uc y HyInXU).

We prove the intermediate claim HyNotClU: y ∉ closure_of X T U.

Assume HyCl: y ∈ closure_of X T U.

Apply FalseE to the current goal.

We prove the intermediate claim HyUc: y ∈ Uc.

An exact proof term for the current goal is (HclU_sub_Uc y HyCl).

An exact proof term for the current goal is (HyNotUc HyUc).

We prove the intermediate claim HyV: y ∈ V0.

Apply (xm (y ∈ V0)) to the current goal.

Assume H.

An exact proof term for the current goal is H.

Assume HyNotV0: y ∉ V0.

Apply FalseE to the current goal.

We prove the intermediate claim HyClU: y ∈ closure_of X T U.

rewrite the current goal using HclEq (from left to right).

An exact proof term for the current goal is (setminusI X V0 y HyX HyNotV0).

An exact proof term for the current goal is (HyNotClU HyClU).

An exact proof term for the current goal is HyV.

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ U ∩ V0.

We will prove z ∈ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HzU: z ∈ U.

An exact proof term for the current goal is (binintersectE1 U V0 z Hz).

We prove the intermediate claim HzV0: z ∈ V0.

An exact proof term for the current goal is (binintersectE2 U V0 z Hz).

We prove the intermediate claim HzCl: z ∈ closure_of X T U.

An exact proof term for the current goal is (subset_of_closure X T U HT HUsubX z HzU).

We prove the intermediate claim HzXminus: z ∈ X ∖ V0.

rewrite the current goal using HclEq (from right to left).

An exact proof term for the current goal is HzCl.

We prove the intermediate claim HzNotV0: z ∉ V0.

An exact proof term for the current goal is (setminusE2 X V0 z HzXminus).

An exact proof term for the current goal is (HzNotV0 HzV0).