Let X, S and s be given.
Assume HS: subbasis_on X S.
Assume Hs: s ∈ S.
We will prove s ∈ generated_topology_from_subbasis X S.
We prove the intermediate claim HT: topology_on X (generated_topology_from_subbasis X S).
An exact proof term for the current goal is (topology_from_subbasis_is_topology X S HS).
Apply (xm (s = Empty)) to the current goal.
Assume Hseq: s = Empty.
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (topology_has_empty X (generated_topology_from_subbasis X S) HT).
Assume Hsne: ¬ (s = Empty).
We prove the intermediate claim HsSubX: s ⊆ X.
We prove the intermediate claim HSsubPow: S ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (S ⊆ 𝒫 X) (⋃ S = X) HS).
We prove the intermediate claim HsPow: s ∈ 𝒫 X.
An exact proof term for the current goal is (HSsubPow s Hs).
An exact proof term for the current goal is (PowerE X s HsPow).
We prove the intermediate claim Hints: intersection_of_family X {s} = s.
An exact proof term for the current goal is (intersection_of_family_singleton_eq X s HsSubX).
We prove the intermediate claim HsingSub: {s} ⊆ S.
Let t be given.
Assume Ht: t ∈ {s}.
We prove the intermediate claim Hteq: t = s.
An exact proof term for the current goal is (SingE s t Ht).
rewrite the current goal using Hteq (from left to right).
An exact proof term for the current goal is Hs.
We prove the intermediate claim HsingPow: {s} ∈ 𝒫 S.
An exact proof term for the current goal is (PowerI S {s} HsingSub).
We prove the intermediate claim HsingFin: finite {s}.
An exact proof term for the current goal is (Sing_finite s).
We prove the intermediate claim HsingFS: {s} ∈ finite_subcollections S.
An exact proof term for the current goal is (SepI (𝒫 S) (λF0 : set ⇒ finite F0) {s} HsingPow HsingFin).
We prove the intermediate claim HsInFinInt: s ∈ finite_intersections_of X S.
rewrite the current goal using Hints (from right to left).
An exact proof term for the current goal is (ReplI (finite_subcollections S) (λF0 : set ⇒ intersection_of_family X F0) {s} HsingFS).
We prove the intermediate claim HsInBasis: s ∈ basis_of_subbasis X S.
An exact proof term for the current goal is (SepI (finite_intersections_of X S) (λb0 : set ⇒ b0 ≠ Empty) s HsInFinInt Hsne).
We prove the intermediate claim HBasis: basis_on X (basis_of_subbasis X S).
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis X S HS).
We prove the intermediate claim HopenGen: s ∈ generated_topology X (basis_of_subbasis X S).
An exact proof term for the current goal is (generated_topology_contains_basis X (basis_of_subbasis X S) HBasis s HsInBasis).
An exact proof term for the current goal is HopenGen.
∎