Let X and B be given.
Assume 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.
Apply set_ext to the current goal.
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).
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).
∎