Let X, T and C be given.
Assume Htop HCsub Href.
We prove the intermediate claim Hleft: ((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)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) Htop).
We prove the intermediate claim Hcore: (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) Hleft).
We prove the intermediate claim HTPowEmpty: T ⊆ 𝒫 X ∧ Empty ∈ T.
An exact proof term for the current goal is (andEL (T ⊆ 𝒫 X ∧ Empty ∈ T) (X ∈ T) Hcore).
We prove the intermediate claim HTsubPow: T ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (T ⊆ 𝒫 X) (Empty ∈ T) HTPowEmpty).
We prove the intermediate claim HXT: X ∈ T.
An exact proof term for the current goal is (andER (T ⊆ 𝒫 X ∧ Empty ∈ T) (X ∈ T) Hcore).
We prove the intermediate claim HUnionClosed: ∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T.
An exact proof term for the current goal is (andER ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T) Hleft).
We prove the intermediate claim HInterClosed: ∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T.
An exact proof term for the current goal is (andER (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) Htop).
We prove the intermediate claim HBasis: basis_on X C.
We will prove (C ⊆ 𝒫 X ∧ (∀x ∈ X, ∃c ∈ C, x ∈ c) ∧ (∀b1 ∈ C, ∀b2 ∈ C, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ C, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)).
Apply and3I to the current goal.
Let c be given.
Assume HcC.
An exact proof term for the current goal is (HTsubPow c (HCsub c HcC)).
Let x be given.
Assume HxX.
We prove the intermediate claim Hex: ∃c ∈ C, x ∈ c ∧ c ⊆ X.
An exact proof term for the current goal is (Href X HXT x HxX).
Apply Hex to the current goal.
Let c be given.
Assume Hpair.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (andEL (c ∈ C) (x ∈ c ∧ c ⊆ X) Hpair).
We prove the intermediate claim Hcprop: x ∈ c ∧ c ⊆ X.
An exact proof term for the current goal is (andER (c ∈ C) (x ∈ c ∧ c ⊆ X) Hpair).
We prove the intermediate claim Hxc: x ∈ c.
An exact proof term for the current goal is (andEL (x ∈ c) (c ⊆ X) Hcprop).
We use c to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HcC.
An exact proof term for the current goal is Hxc.
Let c1 be given.
Assume Hc1C.
Let c2 be given.
Assume Hc2C.
Let x be given.
Assume Hxc1 Hxc2.
We prove the intermediate claim Hc1T: c1 ∈ T.
An exact proof term for the current goal is (HCsub c1 Hc1C).
We prove the intermediate claim Hc2T: c2 ∈ T.
An exact proof term for the current goal is (HCsub c2 Hc2C).
We prove the intermediate claim HcapT: c1 ∩ c2 ∈ T.
An exact proof term for the current goal is (HInterClosed c1 Hc1T c2 Hc2T).
We prove the intermediate claim HxCap: x ∈ c1 ∩ c2.
An exact proof term for the current goal is (binintersectI c1 c2 x Hxc1 Hxc2).
We prove the intermediate claim Hex: ∃c3 ∈ C, x ∈ c3 ∧ c3 ⊆ c1 ∩ c2.
An exact proof term for the current goal is (Href (c1 ∩ c2) HcapT x HxCap).
An exact proof term for the current goal is Hex.
We prove the intermediate claim Hgen_sub_T: generated_topology X C ⊆ T.
Let U be given.
Assume HUgen: U ∈ generated_topology X C.
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U (SepE1 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ C, x0 ∈ b0 ∧ b0 ⊆ U0) U HUgen)).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃c ∈ C, x ∈ c ∧ c ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ C, x0 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
Set Fam to be the term {c ∈ C|c ⊆ U} of type set.
We prove the intermediate claim HFamSubC: Fam ⊆ C.
Let c be given.
Assume HcFam.
An exact proof term for the current goal is (SepE1 C (λc0 : set ⇒ c0 ⊆ U) c HcFam).
We prove the intermediate claim HFamSubT: Fam ⊆ T.
Let c be given.
Assume HcFam.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (HFamSubC c HcFam).
An exact proof term for the current goal is (HCsub c HcC).
We prove the intermediate claim HFamPowT: Fam ∈ 𝒫 T.
An exact proof term for the current goal is (PowerI T Fam HFamSubT).
We prove the intermediate claim HUnionSubU: ⋃ Fam ⊆ U.
Let x be given.
Assume HxUnion.
Apply UnionE_impred Fam x HxUnion to the current goal.
Let c be given.
Assume Hxc HcFam.
We prove the intermediate claim Hcprop: c ⊆ U.
An exact proof term for the current goal is (SepE2 C (λc0 : set ⇒ c0 ⊆ U) c HcFam).
An exact proof term for the current goal is (Hcprop x Hxc).
We prove the intermediate claim HUsubUnion: U ⊆ ⋃ Fam.
Let x be given.
Assume HxU.
We prove the intermediate claim Hex: ∃c ∈ C, x ∈ c ∧ c ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Apply Hex to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (andEL (c ∈ C) (x ∈ c ∧ c ⊆ U) Hcpair).
We prove the intermediate claim Hcprop: x ∈ c ∧ c ⊆ U.
An exact proof term for the current goal is (andER (c ∈ C) (x ∈ c ∧ c ⊆ U) Hcpair).
We prove the intermediate claim Hxc: x ∈ c.
An exact proof term for the current goal is (andEL (x ∈ c) (c ⊆ U) Hcprop).
We prove the intermediate claim HcsubU: c ⊆ U.
An exact proof term for the current goal is (andER (x ∈ c) (c ⊆ U) Hcprop).
We prove the intermediate claim HcFam: c ∈ Fam.
An exact proof term for the current goal is (SepI C (λc0 : set ⇒ c0 ⊆ U) c HcC HcsubU).
An exact proof term for the current goal is (UnionI Fam x c Hxc HcFam).
We prove the intermediate claim HUnionEqU: ⋃ Fam = U.
Apply set_ext to the current goal.
Let x be given.
Assume HxUnion.
An exact proof term for the current goal is (HUnionSubU x HxUnion).
Let x be given.
Assume HxU.
An exact proof term for the current goal is (HUsubUnion x HxU).
We prove the intermediate claim HUnionInT: ⋃ Fam ∈ T.
An exact proof term for the current goal is (HUnionClosed Fam HFamPowT).
rewrite the current goal using HUnionEqU (from right to left).
An exact proof term for the current goal is HUnionInT.
We prove the intermediate claim HT_sub_gen: T ⊆ generated_topology X C.
Let U be given.
Assume HU: U ∈ T.
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U (HTsubPow U HU)).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃c ∈ C, x ∈ c ∧ c ⊆ U.
Let x be given.
Assume HxU.
An exact proof term for the current goal is (Href U HU x HxU).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ C, x0 ∈ b0 ∧ b0 ⊆ U0) U (PowerI X U HUsubX) HUprop).
We prove the intermediate claim HEqual: generated_topology X C = T.
Apply set_ext to the current goal.
Let U be given.
Assume HUgen.
An exact proof term for the current goal is (Hgen_sub_T U HUgen).
Let U be given.
Assume HU.
An exact proof term for the current goal is (HT_sub_gen U HU).
Apply andI to the current goal.
An exact proof term for the current goal is HBasis.
An exact proof term for the current goal is HEqual.
∎