Let X and Tx be given.
Assume HTx: topology_on X Tx.
Assume Hloc: ∀x : set, x ∈ X → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ Baire_space U (subspace_topology X Tx U).
We will prove Baire_space X Tx.
We will prove topology_on X Tx ∧ ∀U0 : set, U0 ⊆ Tx → countable_set U0 → (∀u : set, u ∈ U0 → u ∈ Tx ∧ dense_in u X Tx) → dense_in (intersection_over_family X U0) X Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let U0 be given.
Assume HU0sub: U0 ⊆ Tx.
Assume HU0count: countable_set U0.
Assume HUdense: ∀u : set, u ∈ U0 → u ∈ Tx ∧ dense_in u X Tx.
Set I to be the term intersection_over_family X U0.
We will prove dense_in I X Tx.
We will prove closure_of X Tx I = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space X Tx I HTx).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ closure_of X Tx I.
We prove the intermediate claim Hcliff: x ∈ closure_of X Tx I ↔ (∀W ∈ Tx, x ∈ W → W ∩ I ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx I x HTx HxX).
Apply (iffER (x ∈ closure_of X Tx I) (∀W ∈ Tx, x ∈ W → W ∩ I ≠ Empty) Hcliff) to the current goal.
Let W be given.
Assume HWTx: W ∈ Tx.
Assume HxW: x ∈ W.
We will prove W ∩ I ≠ Empty.
Apply (Hloc x HxX) to the current goal.
Let U be given.
Assume HU: U ∈ Tx ∧ x ∈ U ∧ Baire_space U (subspace_topology X Tx U).
We prove the intermediate claim HU12: (U ∈ Tx ∧ x ∈ U).
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (Baire_space U (subspace_topology X Tx U)) HU).
We prove the intermediate claim HUb: Baire_space U (subspace_topology X Tx U).
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (Baire_space U (subspace_topology X Tx U)) HU).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HU12).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HU12).
We prove the intermediate claim HUsX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HtopU: topology_on U (subspace_topology X Tx U).
An exact proof term for the current goal is (andEL (topology_on U (subspace_topology X Tx U)) (∀Ufam : set, Ufam ⊆ (subspace_topology X Tx U) → countable_set Ufam → (∀u0 : set, u0 ∈ Ufam → u0 ∈ (subspace_topology X Tx U) ∧ dense_in u0 U (subspace_topology X Tx U)) → dense_in (intersection_over_family U Ufam) U (subspace_topology X Tx U)) HUb).
We prove the intermediate claim HBUprop: ∀Ufam : set, Ufam ⊆ (subspace_topology X Tx U) → countable_set Ufam → (∀u0 : set, u0 ∈ Ufam → u0 ∈ (subspace_topology X Tx U) ∧ dense_in u0 U (subspace_topology X Tx U)) → dense_in (intersection_over_family U Ufam) U (subspace_topology X Tx U).
An exact proof term for the current goal is (andER (topology_on U (subspace_topology X Tx U)) (∀Ufam : set, Ufam ⊆ (subspace_topology X Tx U) → countable_set Ufam → (∀u0 : set, u0 ∈ Ufam → u0 ∈ (subspace_topology X Tx U) ∧ dense_in u0 U (subspace_topology X Tx U)) → dense_in (intersection_over_family U Ufam) U (subspace_topology X Tx U)) HUb).
Set Ufam to be the term {u ∩ U|u ∈ U0}.
We prove the intermediate claim HUfam_count: countable_set Ufam.
An exact proof term for the current goal is (countable_image U0 HU0count (λu : set ⇒ u ∩ U)).
We prove the intermediate claim HUfam_sub: Ufam ⊆ subspace_topology X Tx U.
Let A be given.
Assume HA: A ∈ Ufam.
We prove the intermediate claim Hexu: ∃u : set, u ∈ U0 ∧ A = u ∩ U.
An exact proof term for the current goal is (ReplE U0 (λu0 : set ⇒ u0 ∩ U) A HA).
Apply Hexu to the current goal.
Let u be given.
Assume Hu: u ∈ U0 ∧ A = u ∩ U.
We prove the intermediate claim Hu0: u ∈ U0.
An exact proof term for the current goal is (andEL (u ∈ U0) (A = u ∩ U) Hu).
We prove the intermediate claim HAeq: A = u ∩ U.
An exact proof term for the current goal is (andER (u ∈ U0) (A = u ∩ U) Hu).
We prove the intermediate claim HuTx: u ∈ Tx.
An exact proof term for the current goal is (andEL (u ∈ Tx) (dense_in u X Tx) (HUdense u Hu0)).
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx U u HuTx).
We prove the intermediate claim HUfam_prop: ∀A : set, A ∈ Ufam → A ∈ (subspace_topology X Tx U) ∧ dense_in A U (subspace_topology X Tx U).
Let A be given.
Assume HA: A ∈ Ufam.
We prove the intermediate claim Hexu: ∃u : set, u ∈ U0 ∧ A = u ∩ U.
An exact proof term for the current goal is (ReplE U0 (λu0 : set ⇒ u0 ∩ U) A HA).
Apply Hexu to the current goal.
Let u be given.
Assume Hu: u ∈ U0 ∧ A = u ∩ U.
We prove the intermediate claim Hu0: u ∈ U0.
An exact proof term for the current goal is (andEL (u ∈ U0) (A = u ∩ U) Hu).
We prove the intermediate claim HAeq: A = u ∩ U.
An exact proof term for the current goal is (andER (u ∈ U0) (A = u ∩ U) Hu).
We prove the intermediate claim HuPack: u ∈ Tx ∧ dense_in u X Tx.
An exact proof term for the current goal is (HUdense u Hu0).
We prove the intermediate claim HuTx: u ∈ Tx.
An exact proof term for the current goal is (andEL (u ∈ Tx) (dense_in u X Tx) HuPack).
We prove the intermediate claim Hud: dense_in u X Tx.
An exact proof term for the current goal is (andER (u ∈ Tx) (dense_in u X Tx) HuPack).
rewrite the current goal using HAeq (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is (subspace_topologyI X Tx U u HuTx).
We will prove dense_in (u ∩ U) U (subspace_topology X Tx U).
We will prove closure_of U (subspace_topology X Tx U) (u ∩ U) = U.
We prove the intermediate claim HUsub: (u ∩ U) ⊆ U.
An exact proof term for the current goal is (binintersect_Subq_2 u U).
We prove the intermediate claim HclEq: closure_of U (subspace_topology X Tx U) (u ∩ U) = (closure_of X Tx (u ∩ U)) ∩ U.
An exact proof term for the current goal is (closure_in_subspace X Tx U (u ∩ U) HTx HUsX HUsub).
rewrite the current goal using HclEq (from left to right).
Apply set_ext to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 (closure_of X Tx (u ∩ U)) U).
Let y be given.
Assume HyU: y ∈ U.
We will prove y ∈ (closure_of X Tx (u ∩ U)) ∩ U.
Apply binintersectI to the current goal.
We will prove y ∈ closure_of X Tx (u ∩ U).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HUsX y HyU).
We prove the intermediate claim HudEq: closure_of X Tx u = X.
An exact proof term for the current goal is Hud.
We prove the intermediate claim Hyclu: y ∈ closure_of X Tx u.
rewrite the current goal using HudEq (from left to right).
An exact proof term for the current goal is HyX.
We prove the intermediate claim Hcliff2: y ∈ closure_of X Tx (u ∩ U) ↔ (∀V ∈ Tx, y ∈ V → V ∩ (u ∩ U) ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx (u ∩ U) y HTx HyX).
Apply (iffER (y ∈ closure_of X Tx (u ∩ U)) (∀V ∈ Tx, y ∈ V → V ∩ (u ∩ U) ≠ Empty) Hcliff2) to the current goal.
Let V be given.
Assume HVTx: V ∈ Tx.
Assume HyV: y ∈ V.
We will prove V ∩ (u ∩ U) ≠ Empty.
We prove the intermediate claim HVU: V ∩ U ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_axiom X Tx HTx V HVTx U HUinTx).
We prove the intermediate claim HyVU: y ∈ V ∩ U.
An exact proof term for the current goal is (binintersectI V U y HyV HyU).
We prove the intermediate claim Hiffu: y ∈ closure_of X Tx u ↔ (∀S ∈ Tx, y ∈ S → S ∩ u ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx u y HTx HyX).
We prove the intermediate claim HyCondU: ∀S ∈ Tx, y ∈ S → S ∩ u ≠ Empty.
An exact proof term for the current goal is (iffEL (y ∈ closure_of X Tx u) (∀S ∈ Tx, y ∈ S → S ∩ u ≠ Empty) Hiffu Hyclu).
We prove the intermediate claim Hne1: (V ∩ U) ∩ u ≠ Empty.
An exact proof term for the current goal is (HyCondU (V ∩ U) HVU HyVU).
Apply (nonempty_has_element ((V ∩ U) ∩ u) Hne1) to the current goal.
Let t be given.
Assume Ht: t ∈ (V ∩ U) ∩ u.
We prove the intermediate claim HtVU: t ∈ V ∩ U.
An exact proof term for the current goal is (binintersectE1 (V ∩ U) u t Ht).
We prove the intermediate claim HtV: t ∈ V.
An exact proof term for the current goal is (binintersectE1 V U t HtVU).
We prove the intermediate claim HtU: t ∈ U.
An exact proof term for the current goal is (binintersectE2 V U t HtVU).
We prove the intermediate claim Htu: t ∈ u.
An exact proof term for the current goal is (binintersectE2 (V ∩ U) u t Ht).
We prove the intermediate claim HtUu: t ∈ u ∩ U.
An exact proof term for the current goal is (binintersectI u U t Htu HtU).
We prove the intermediate claim HtVUU: t ∈ V ∩ (u ∩ U).
An exact proof term for the current goal is (binintersectI V (u ∩ U) t HtV HtUu).
Assume Hem: V ∩ (u ∩ U) = Empty.
We prove the intermediate claim HtE: t ∈ Empty.
rewrite the current goal using Hem (from right to left).
An exact proof term for the current goal is HtVUU.
An exact proof term for the current goal is (EmptyE t HtE).
An exact proof term for the current goal is HyU.
We prove the intermediate claim HdenseInt: dense_in (intersection_over_family U Ufam) U (subspace_topology X Tx U).
An exact proof term for the current goal is (HBUprop Ufam HUfam_sub HUfam_count HUfam_prop).
We prove the intermediate claim HdenseEq: closure_of U (subspace_topology X Tx U) (intersection_over_family U Ufam) = U.
An exact proof term for the current goal is HdenseInt.
Set WU to be the term W ∩ U.
We prove the intermediate claim HWU_in: WU ∈ subspace_topology X Tx U.
An exact proof term for the current goal is (subspace_topologyI X Tx U W HWTx).
We prove the intermediate claim HxWU: x ∈ WU.
An exact proof term for the current goal is (binintersectI W U x HxW HxU).
We prove the intermediate claim HWUne: WU ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty WU x HxWU).
We prove the intermediate claim HWUmeets: WU ∩ (intersection_over_family U Ufam) ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open (intersection_over_family U Ufam) U (subspace_topology X Tx U) WU HtopU HdenseEq HWU_in HWUne).
Apply (nonempty_has_element (WU ∩ (intersection_over_family U Ufam)) HWUmeets) to the current goal.
Let y be given.
Assume Hycap: y ∈ WU ∩ (intersection_over_family U Ufam).
We prove the intermediate claim HyWU: y ∈ WU.
An exact proof term for the current goal is (binintersectE1 WU (intersection_over_family U Ufam) y Hycap).
We prove the intermediate claim HyInt: y ∈ intersection_over_family U Ufam.
An exact proof term for the current goal is (binintersectE2 WU (intersection_over_family U Ufam) y Hycap).
We prove the intermediate claim HyW: y ∈ W.
An exact proof term for the current goal is (binintersectE1 W U y HyWU).
We prove the intermediate claim HyI: y ∈ I.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (intersection_of_familyE1 U Ufam y HyInt).
Apply (intersection_of_familyI X U0 y (HUsX y HyU)) to the current goal.
Let T be given.
Assume HT: T ∈ U0.
We prove the intermediate claim HTUfam: (T ∩ U) ∈ Ufam.
An exact proof term for the current goal is (ReplI U0 (λu0 : set ⇒ u0 ∩ U) T HT).
We prove the intermediate claim HyAll: ∀A : set, A ∈ Ufam → y ∈ A.
An exact proof term for the current goal is (intersection_of_familyE2 U Ufam y HyInt).
We prove the intermediate claim HyTU: y ∈ T ∩ U.
An exact proof term for the current goal is (HyAll (T ∩ U) HTUfam).
An exact proof term for the current goal is (binintersectE1 T U y HyTU).
Assume Hem: W ∩ I = Empty.
We prove the intermediate claim HyWI: y ∈ W ∩ I.
An exact proof term for the current goal is (binintersectI W I y HyW HyI).
We prove the intermediate claim HyE: y ∈ Empty.
rewrite the current goal using Hem (from right to left).
An exact proof term for the current goal is HyWI.
An exact proof term for the current goal is (EmptyE y HyE).
∎