Let X and B be given.
Assume HBasis.
We prove the intermediate claim HBsub: B ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (B ⊆ 𝒫 X) (∀x ∈ X, ∃b ∈ B, x ∈ b) (andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ B, x ∈ b)) (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBasis)).
Let U be given.
Assume Hex.
We prove the intermediate claim HUGen: U ∈ generated_topology X B.
Apply Hex to the current goal.
Let Fam be given.
Assume HFampair.
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 B.
An exact proof term for the current goal is (andEL (Fam ∈ 𝒫 B) (⋃ Fam = U) HFampair).
We prove the intermediate claim HUnionEq: ⋃ Fam = U.
An exact proof term for the current goal is (andER (Fam ∈ 𝒫 B) (⋃ Fam = U) HFampair).
We prove the intermediate claim HFamSubB: Fam ⊆ B.
An exact proof term for the current goal is (PowerE B Fam HFamPow).
We prove the intermediate claim HFamSubX: Fam ⊆ 𝒫 X.
Let b be given.
Assume HbFam.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (HFamSubB b HbFam).
An exact proof term for the current goal is (HBsub b HbB).
We prove the intermediate claim HUnionSubX: ⋃ Fam ⊆ X.
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 HbSubX: b ⊆ X.
An exact proof term for the current goal is (PowerE X b (HFamSubX b HbFam)).
An exact proof term for the current goal is (HbSubX x Hxb).
We prove the intermediate claim HUnionSubU: ⋃ Fam ⊆ U.
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is (Subq_ref U).
We prove the intermediate claim HUsubUnion: U ⊆ ⋃ Fam.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is (Subq_ref (⋃ Fam)).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (Subq_tra U (⋃ Fam) X HUsubUnion HUnionSubX).
We prove the intermediate claim HUpropU: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.
Let x be given.
Assume HxU.
We prove the intermediate claim HxUnion: x ∈ ⋃ Fam.
An exact proof term for the current goal is (HUsubUnion x HxU).
Apply UnionE_impred Fam x HxUnion to the current goal.
Let b be given.
Assume Hxb HbFam.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (HFamSubB b HbFam).
We prove the intermediate claim HbSubUnion: b ⊆ ⋃ Fam.
Let y be given.
Assume Hyb.
An exact proof term for the current goal is (UnionI Fam y b Hyb HbFam).
We prove the intermediate claim HbSubU: b ⊆ U.
An exact proof term for the current goal is (Subq_tra b (⋃ Fam) U HbSubUnion HUnionSubU).
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb.
An exact proof term for the current goal is HbSubU.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U (PowerI X U HUsubX) HUpropU).
An exact proof term for the current goal is (andI (topology_on X (generated_topology X B)) (U ∈ generated_topology X B) (lemma_topology_from_basis X B HBasis) HUGen).
∎