Let X and Fam be given.
Assume HfamTop: ∀T ∈ Fam, topology_on X T.
We will prove ∃Tmin, topology_on X Tmin ∧ (∀T ∈ Fam, T ⊆ Tmin) ∧ (∀T', topology_on X T' ∧ (∀T ∈ Fam, T ⊆ T') → Tmin ⊆ T') ∧ ∃Tmax, topology_on X Tmax ∧ (∀T ∈ Fam, Tmax ⊆ T) ∧ (∀T', topology_on X T' ∧ (∀T ∈ Fam, T' ⊆ T) → T' ⊆ Tmax).
Set Tmax to be the term Intersection_Fam X Fam.
Set Tmin to be the term generated_topology_from_subbasis X (⋃ Fam ∪ {X}).
We prove the intermediate claim HTmax_topology: topology_on X Tmax.
Apply (xm (∃T : set, T ∈ Fam)) to the current goal.
Assume HFamNonempty: ∃T : set, T ∈ Fam.
An exact proof term for the current goal is (ex13_4a_intersection_topology X Fam HFamNonempty HfamTop).
Assume HFamEmpty: ¬ (∃T : set, T ∈ Fam).
rewrite the current goal using (Intersection_Fam_empty_eq X Fam HFamEmpty) (from left to right).
An exact proof term for the current goal is (discrete_topology_on X).
We prove the intermediate claim HTmax_subset_all: ∀T ∈ Fam, Tmax ⊆ T.
Let T be given.
Assume HT: T ∈ Fam.
Let U be given.
Assume HU: U ∈ Tmax.
We prove the intermediate claim HUinT: U ∈ T.
We prove the intermediate claim HUinAllT: ∀T0 : set, T0 ∈ Fam → U ∈ T0.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 ⇒ ∀T0 : set, T0 ∈ Fam → U0 ∈ T0) U HU).
An exact proof term for the current goal is (HUinAllT T HT).
An exact proof term for the current goal is HUinT.
We prove the intermediate claim HTmax_maximal: ∀T', topology_on X T' ∧ (∀T ∈ Fam, T' ⊆ T) → T' ⊆ Tmax.
Let T' be given.
Assume HT'_cond.
We prove the intermediate claim HT'_top: topology_on X T'.
An exact proof term for the current goal is (andEL (topology_on X T') (∀T ∈ Fam, T' ⊆ T) HT'_cond).
We prove the intermediate claim HT'_sub_all: ∀T ∈ Fam, T' ⊆ T.
An exact proof term for the current goal is (andER (topology_on X T') (∀T ∈ Fam, T' ⊆ T) HT'_cond).
Let U be given.
Assume HU: U ∈ T'.
We prove the intermediate claim HUinPower: U ∈ 𝒫 X.
We prove the intermediate claim HT'_sub_PowerX: T' ⊆ 𝒫 X.
We prove the intermediate claim H1: ((T' ⊆ 𝒫 X ∧ Empty ∈ T') ∧ X ∈ T') ∧ (∀UFam ∈ 𝒫 T', ⋃ UFam ∈ T').
An exact proof term for the current goal is (andEL (((T' ⊆ 𝒫 X ∧ Empty ∈ T') ∧ X ∈ T') ∧ (∀UFam ∈ 𝒫 T', ⋃ UFam ∈ T')) (∀U0 ∈ T', ∀V ∈ T', U0 ∩ V ∈ T') HT'_top).
We prove the intermediate claim H2: (T' ⊆ 𝒫 X ∧ Empty ∈ T') ∧ X ∈ T'.
An exact proof term for the current goal is (andEL ((T' ⊆ 𝒫 X ∧ Empty ∈ T') ∧ X ∈ T') (∀UFam ∈ 𝒫 T', ⋃ UFam ∈ T') H1).
We prove the intermediate claim H3: T' ⊆ 𝒫 X ∧ Empty ∈ T'.
An exact proof term for the current goal is (andEL (T' ⊆ 𝒫 X ∧ Empty ∈ T') (X ∈ T') H2).
An exact proof term for the current goal is (andEL (T' ⊆ 𝒫 X) (Empty ∈ T') H3).
An exact proof term for the current goal is (HT'_sub_PowerX U HU).
We prove the intermediate claim HUinAllT: ∀T ∈ Fam, U ∈ T.
Let T be given.
Assume HT: T ∈ Fam.
We prove the intermediate claim HT'subT: T' ⊆ T.
An exact proof term for the current goal is (HT'_sub_all T HT).
An exact proof term for the current goal is (HT'subT U HU).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HUinPower HUinAllT).
We prove the intermediate claim HUnionFam_subbasis: subbasis_on X (⋃ Fam ∪ {X}).
We will prove (⋃ Fam ∪ {X}) ⊆ 𝒫 X ∧ ⋃ (⋃ Fam ∪ {X}) = X.
Apply andI to the current goal.
Let U be given.
Assume HU: U ∈ ⋃ Fam ∪ {X}.
We will prove U ∈ 𝒫 X.
Apply (binunionE' (⋃ Fam) {X} U (U ∈ 𝒫 X)) to the current goal.
Assume HUinUnion: U ∈ ⋃ Fam.
Apply UnionE_impred Fam U HUinUnion to the current goal.
Let T be given.
Assume HUT: U ∈ T.
Assume HT: T ∈ Fam.
We prove the intermediate claim HTtop: topology_on X T.
An exact proof term for the current goal is (HfamTop T HT).
We prove the intermediate claim H1: ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T).
An exact proof term for the current goal is (andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T)) (∀U0 ∈ T, ∀V ∈ T, U0 ∩ V ∈ T) HTtop).
We prove the intermediate claim H2: (T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T.
An exact proof term for the current goal is (andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T) H1).
We prove the intermediate claim H3: T ⊆ 𝒫 X ∧ Empty ∈ T.
An exact proof term for the current goal is (andEL (T ⊆ 𝒫 X ∧ Empty ∈ T) (X ∈ T) H2).
We prove the intermediate claim HTsub: T ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (T ⊆ 𝒫 X) (Empty ∈ T) H3).
An exact proof term for the current goal is (HTsub U HUT).
Assume HUinSing: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HUinSing).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (PowerI X X (Subq_ref X)).
An exact proof term for the current goal is HU.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ (⋃ Fam ∪ {X}).
We will prove x ∈ X.
Apply UnionE_impred (⋃ Fam ∪ {X}) x Hx to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HU: U ∈ ⋃ Fam ∪ {X}.
Apply (binunionE' (⋃ Fam) {X} U (x ∈ X)) to the current goal.
Assume HUinUnion: U ∈ ⋃ Fam.
Apply UnionE_impred Fam U HUinUnion to the current goal.
Let T be given.
Assume HUT: U ∈ T.
Assume HT: T ∈ Fam.
We prove the intermediate claim HTtop: topology_on X T.
An exact proof term for the current goal is (HfamTop T HT).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X T U HTtop HUT).
An exact proof term for the current goal is (HUsubX x HxU).
Assume HUinSing: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HUinSing).
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HU.
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ ⋃ (⋃ Fam ∪ {X}).
We prove the intermediate claim HX_in_subbasis: X ∈ ⋃ Fam ∪ {X}.
An exact proof term for the current goal is (binunionI2 (⋃ Fam) {X} X (SingI X)).
An exact proof term for the current goal is (UnionI (⋃ Fam ∪ {X}) x X HxX HX_in_subbasis).
We prove the intermediate claim HTmin_topology: topology_on X Tmin.
An exact proof term for the current goal is (topology_from_subbasis_is_topology X (⋃ Fam ∪ {X}) HUnionFam_subbasis).
We prove the intermediate claim HTmin_contains_all: ∀T ∈ Fam, T ⊆ Tmin.
Let T be given.
Assume HT: T ∈ Fam.
Let U be given.
Assume HU: U ∈ T.
We prove the intermediate claim HUinUnionFam: U ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam U T HU HT).
Apply (xm (U = Empty)) to the current goal.
Assume HUempty: U = Empty.
We prove the intermediate claim HEmptyinTmin: Empty ∈ Tmin.
We prove the intermediate claim H1: ((Tmin ⊆ 𝒫 X ∧ Empty ∈ Tmin) ∧ X ∈ Tmin) ∧ (∀UFam ∈ 𝒫 Tmin, ⋃ UFam ∈ Tmin).
An exact proof term for the current goal is (andEL (((Tmin ⊆ 𝒫 X ∧ Empty ∈ Tmin) ∧ X ∈ Tmin) ∧ (∀UFam ∈ 𝒫 Tmin, ⋃ UFam ∈ Tmin)) (∀U0 ∈ Tmin, ∀V ∈ Tmin, U0 ∩ V ∈ Tmin) HTmin_topology).
We prove the intermediate claim H2: (Tmin ⊆ 𝒫 X ∧ Empty ∈ Tmin) ∧ X ∈ Tmin.
An exact proof term for the current goal is (andEL ((Tmin ⊆ 𝒫 X ∧ Empty ∈ Tmin) ∧ X ∈ Tmin) (∀UFam ∈ 𝒫 Tmin, ⋃ UFam ∈ Tmin) H1).
We prove the intermediate claim H3: Tmin ⊆ 𝒫 X ∧ Empty ∈ Tmin.
An exact proof term for the current goal is (andEL (Tmin ⊆ 𝒫 X ∧ Empty ∈ Tmin) (X ∈ Tmin) H2).
An exact proof term for the current goal is (andER (Tmin ⊆ 𝒫 X) (Empty ∈ Tmin) H3).
rewrite the current goal using HUempty (from left to right).
An exact proof term for the current goal is HEmptyinTmin.
Assume HUnonempty: U ≠ Empty.
We prove the intermediate claim HUinSubbasis: U ∈ ⋃ Fam ∪ {X}.
An exact proof term for the current goal is (binunionI1 (⋃ Fam) {X} U HUinUnionFam).
We prove the intermediate claim HUinBasis: U ∈ basis_of_subbasis X (⋃ Fam ∪ {X}).
An exact proof term for the current goal is (subbasis_elem_in_basis X (⋃ Fam ∪ {X}) U HUnionFam_subbasis HUinSubbasis HUnonempty).
We prove the intermediate claim HBasis: basis_on X (basis_of_subbasis X (⋃ Fam ∪ {X})).
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis X (⋃ Fam ∪ {X}) HUnionFam_subbasis).
An exact proof term for the current goal is (basis_in_generated X (basis_of_subbasis X (⋃ Fam ∪ {X})) U HBasis HUinBasis).
We prove the intermediate claim HTmin_minimal: ∀T', topology_on X T' ∧ (∀T ∈ Fam, T ⊆ T') → Tmin ⊆ T'.
Let T' be given.
Assume HT'_cond.
We prove the intermediate claim HT'_top: topology_on X T'.
An exact proof term for the current goal is (andEL (topology_on X T') (∀T ∈ Fam, T ⊆ T') HT'_cond).
We prove the intermediate claim HT'_contains_all: ∀T ∈ Fam, T ⊆ T'.
An exact proof term for the current goal is (andER (topology_on X T') (∀T ∈ Fam, T ⊆ T') HT'_cond).
We prove the intermediate claim HSubbasis_sub_T': ⋃ Fam ∪ {X} ⊆ T'.
Let U be given.
Assume HU: U ∈ ⋃ Fam ∪ {X}.
Apply (binunionE' (⋃ Fam) {X} U (U ∈ T')) to the current goal.
Assume HUinUnion: U ∈ ⋃ Fam.
Apply UnionE_impred Fam U HUinUnion to the current goal.
Let T be given.
Assume HUT: U ∈ T.
Assume HT: T ∈ Fam.
We prove the intermediate claim HTsubT': T ⊆ T'.
An exact proof term for the current goal is (HT'_contains_all T HT).
An exact proof term for the current goal is (HTsubT' U HUT).
Assume HUinSing: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HUinSing).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (topology_has_X X T' HT'_top).
An exact proof term for the current goal is HU.
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal X (⋃ Fam ∪ {X}) T' HUnionFam_subbasis HT'_top HSubbasis_sub_T').
We use Tmin to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTmin_topology.
An exact proof term for the current goal is HTmin_contains_all.
An exact proof term for the current goal is HTmin_minimal.
We use Tmax to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTmax_topology.
An exact proof term for the current goal is HTmax_subset_all.
An exact proof term for the current goal is HTmax_maximal.
∎