Let X, B and T be given.
Assume HBasis HT HBsub.
We prove the intermediate claim HUnionClosed: ∀Fam ∈ 𝒫 T, ⋃ Fam ∈ T.
An exact proof term for the current goal is (andER ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) (∀Fam ∈ 𝒫 T, ⋃ Fam ∈ T) (andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀Fam ∈ 𝒫 T, ⋃ Fam ∈ T)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) HT)).
We will prove generated_topology X B ⊆ T.
Let U be given.
Assume HU.
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 HFamPowB: Fam ∈ 𝒫 B.
Apply PowerI B Fam to the current goal.
Let b be given.
Assume HbFam.
An exact proof term for the current goal is (SepE1 B (λb0 : set ⇒ b0 ⊆ U) b HbFam).
We prove the intermediate claim HUnionEq: ⋃ Fam = U.
Apply set_ext to the current goal.
Let x be given.
Assume HxUnion.
Apply UnionE_impred Fam x HxUnion to the current goal.
Let b be given.
Assume Hxb HbFam.
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.
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 HbT: b ∈ T.
An exact proof term for the current goal is (HBsub b HbB).
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).
We prove the intermediate claim HFamPowT: Fam ∈ 𝒫 T.
Apply PowerI T Fam to the current goal.
Let b be given.
Assume HbFam.
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 HUnionT: ⋃ Fam ∈ T.
An exact proof term for the current goal is (HUnionClosed Fam HFamPowT).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionT.
∎