Let X, B and T be given.
Assume HT: topology_on X T.
Assume HBsub: ∀b ∈ B, b ∈ T.
We will prove finer_than T (generated_topology X B).
We will prove generated_topology X B ⊆ T.
Let U be given.
Assume HU: U ∈ generated_topology X B.
We will prove U ∈ T.
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 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U HU)).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
Set Fam to be the term {b ∈ B|b ⊆ U} of type set.
We prove the intermediate claim HFamSubT: Fam ⊆ T.
Let b be given.
Assume HbFam: b ∈ Fam.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (SepE1 B (λb0 : set ⇒ b0 ⊆ U) b HbFam).
An exact proof term for the current goal is (HBsub b HbB).
We prove the intermediate claim HFamPowT: Fam ∈ 𝒫 T.
Apply PowerI to the current goal.
An exact proof term for the current goal is HFamSubT.
We prove the intermediate claim HUnionInT: ⋃ Fam ∈ T.
An exact proof term for the current goal is (topology_union_axiom X T HT Fam HFamPowT).
We prove the intermediate claim HUnionEq: ⋃ Fam = U.
Apply set_ext to the current goal.
Let x be given.
Assume HxUnion: x ∈ ⋃ Fam.
Apply (UnionE_impred Fam x HxUnion) to the current goal.
Let b be given.
Assume Hxb: x ∈ b.
Assume HbFam: b ∈ Fam.
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (SepE2 B (λb0 : set ⇒ b0 ⊆ U) b HbFam).
An exact proof term for the current goal is (HbsubU x Hxb).
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (SepI B (λb0 : set ⇒ b0 ⊆ U) b HbB HbsubU).
An exact proof term for the current goal is (UnionI Fam x b Hxb HbFam).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionInT.
∎