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 HUopen.
We prove the intermediate claim HUtop: U ∈ generated_topology X B.
An exact proof term for the current goal is (andER (topology_on X (generated_topology X B)) (U ∈ generated_topology X B) HUopen).
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, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HUtop).
Set Fam to be the term {b ∈ B|b ⊆ U} of type set.
We prove the intermediate claim HFamPow: 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 HUnion_eq: ⋃ 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 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 use Fam to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFamPow.
An exact proof term for the current goal is HUnion_eq.
∎