Let X and B be given.
Assume HBasis.
We prove the intermediate claim HBleft: B ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ B, x ∈ b).
An exact proof term for the current goal is (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).
We prove the intermediate claim HBint: ∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
An exact proof term for the current goal is (andER (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).
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) HBleft).
We prove the intermediate claim HBcov: ∀x ∈ X, ∃b ∈ B, x ∈ b.
An exact proof term for the current goal is (andER (B ⊆ 𝒫 X) (∀x ∈ X, ∃b ∈ B, x ∈ b) HBleft).
We prove the intermediate claim proofA: generated_topology X B ⊆ 𝒫 X.
Let U be given.
Assume HU: U ∈ generated_topology X B.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim proofB: Empty ∈ generated_topology X B.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) Empty (Empty_In_Power X) (λx HxEmpty ⇒ EmptyE x HxEmpty (∃b ∈ B, x ∈ b ∧ b ⊆ Empty))).
We prove the intermediate claim proofC: X ∈ generated_topology X B.
We prove the intermediate claim HXprop: ∀x ∈ X, ∃b ∈ B, x ∈ b ∧ b ⊆ X.
Let x be given.
Assume HxX.
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b.
An exact proof term for the current goal is (HBcov x HxX).
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) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b) Hbpair).
We prove the intermediate claim HbsubX: b ⊆ X.
An exact proof term for the current goal is (PowerE X b (HBsub b HbB)).
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 HbsubX.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) X (Self_In_Power X) HXprop).
We prove the intermediate claim proofD: ∀UFam ∈ 𝒫 (generated_topology X B), ⋃ UFam ∈ generated_topology X B.
Let UFam be given.
Assume Hfam: UFam ∈ 𝒫 (generated_topology X B).
We prove the intermediate claim HsubFam: UFam ⊆ generated_topology X B.
An exact proof term for the current goal is (PowerE (generated_topology X B) UFam Hfam).
We prove the intermediate claim HPowUnion: ⋃ UFam ∈ 𝒫 X.
Apply PowerI X (⋃ UFam) to the current goal.
Let x be given.
Assume HxUnion.
Apply UnionE_impred UFam x HxUnion to the current goal.
Let U be given.
Assume HxU HUin.
We prove the intermediate claim HUtop: U ∈ generated_topology X B.
An exact proof term for the current goal is (HsubFam U HUin).
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, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HUtop)).
An exact proof term for the current goal is (HUsubX x HxU).
We prove the intermediate claim HUnionProp: ∀x ∈ ⋃ UFam, ∃b ∈ B, x ∈ b ∧ b ⊆ ⋃ UFam.
Let x be given.
Assume HxUnion.
Apply UnionE_impred UFam x HxUnion to the current goal.
Let U be given.
Assume HxU HUin.
We prove the intermediate claim HUtop: U ∈ generated_topology X B.
An exact proof term for the current goal is (HsubFam U HUin).
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ B, x0 ∈ 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).
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 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.
Let y be given.
Assume Hyb.
Apply UnionI UFam y U (HbSubU y Hyb) HUin to the current goal.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) (⋃ UFam) HPowUnion HUnionProp).
We prove the intermediate claim proofE: ∀U ∈ generated_topology X B, ∀V ∈ generated_topology X B, U ∩ V ∈ generated_topology X B.
Let U be given.
Assume HUtop.
Let V be given.
Assume HVtop.
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ B, x0 ∈ 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).
We prove the intermediate claim HVprop: ∀x0 ∈ V, ∃b ∈ B, x0 ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) V HVtop).
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, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HUtop)).
We prove the intermediate claim HPowCap: U ∩ V ∈ 𝒫 X.
Apply PowerI X (U ∩ V) to the current goal.
Let x be given.
Assume HxCap.
Apply binintersectE U V x HxCap to the current goal.
Assume HxU HxV.
An exact proof term for the current goal is (HUsubX x HxU).
We prove the intermediate claim HCapProp: ∀x ∈ U ∩ V, ∃b ∈ B, x ∈ b ∧ b ⊆ U ∩ V.
Let x be given.
Assume HxCap.
Apply binintersectE U V x HxCap to the current goal.
Assume HxU HxV.
We prove the intermediate claim Hexb1: ∃b1 ∈ B, x ∈ b1 ∧ b1 ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
We prove the intermediate claim Hexb2: ∃b2 ∈ B, x ∈ b2 ∧ b2 ⊆ V.
An exact proof term for the current goal is (HVprop x HxV).
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hbpair1.
We prove the intermediate claim Hb1: b1 ∈ B.
An exact proof term for the current goal is (andEL (b1 ∈ B) (x ∈ b1 ∧ b1 ⊆ U) Hbpair1).
We prove the intermediate claim Hb1prop: x ∈ b1 ∧ b1 ⊆ U.
An exact proof term for the current goal is (andER (b1 ∈ B) (x ∈ b1 ∧ b1 ⊆ U) Hbpair1).
We prove the intermediate claim Hb1x: x ∈ b1.
An exact proof term for the current goal is (andEL (x ∈ b1) (b1 ⊆ U) Hb1prop).
We prove the intermediate claim Hb1Sub: b1 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b1) (b1 ⊆ U) Hb1prop).
Apply Hexb2 to the current goal.
Let b2 be given.
Assume Hbpair2.
We prove the intermediate claim Hb2: b2 ∈ B.
An exact proof term for the current goal is (andEL (b2 ∈ B) (x ∈ b2 ∧ b2 ⊆ V) Hbpair2).
We prove the intermediate claim Hb2prop: x ∈ b2 ∧ b2 ⊆ V.
An exact proof term for the current goal is (andER (b2 ∈ B) (x ∈ b2 ∧ b2 ⊆ V) Hbpair2).
We prove the intermediate claim Hb2x: x ∈ b2.
An exact proof term for the current goal is (andEL (x ∈ b2) (b2 ⊆ V) Hb2prop).
We prove the intermediate claim Hb2Sub: b2 ⊆ V.
An exact proof term for the current goal is (andER (x ∈ b2) (b2 ⊆ V) Hb2prop).
We prove the intermediate claim Hexb3: ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
An exact proof term for the current goal is (HBint b1 Hb1 b2 Hb2 x Hb1x Hb2x).
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hbpair3.
We prove the intermediate claim Hb3: b3 ∈ B.
An exact proof term for the current goal is (andEL (b3 ∈ B) (x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) Hbpair3).
We prove the intermediate claim Hb3prop: x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
An exact proof term for the current goal is (andER (b3 ∈ B) (x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) Hbpair3).
We prove the intermediate claim HxB3: x ∈ b3.
An exact proof term for the current goal is (andEL (x ∈ b3) (b3 ⊆ b1 ∩ b2) Hb3prop).
We prove the intermediate claim Hb3Sub: b3 ⊆ b1 ∩ b2.
An exact proof term for the current goal is (andER (x ∈ b3) (b3 ⊆ b1 ∩ b2) Hb3prop).
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb3.
Apply andI to the current goal.
An exact proof term for the current goal is HxB3.
Let y be given.
Assume Hyb3.
We prove the intermediate claim Hy_in_b1b2: y ∈ b1 ∩ b2.
An exact proof term for the current goal is (Hb3Sub y Hyb3).
Apply binintersectE b1 b2 y Hy_in_b1b2 to the current goal.
Assume Hyb1 Hyb2.
Apply binintersectI U V y (Hb1Sub y Hyb1) (Hb2Sub y Hyb2) to the current goal.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) (U ∩ V) HPowCap HCapProp).
We will prove generated_topology X B ⊆ 𝒫 X ∧ Empty ∈ generated_topology X B ∧ X ∈ generated_topology X B ∧ (∀UFam ∈ 𝒫 (generated_topology X B), ⋃ UFam ∈ generated_topology X B) ∧ (∀U ∈ generated_topology X B, ∀V ∈ generated_topology X B, U ∩ V ∈ generated_topology X B).
Apply and5I to the current goal.
An exact proof term for the current goal is proofA.
An exact proof term for the current goal is proofB.
An exact proof term for the current goal is proofC.
An exact proof term for the current goal is proofD.
An exact proof term for the current goal is proofE.
∎