Metamath Proof Explorer

Theorem onpsstopbas

Description: The class of ordinal numbers is a proper subclass of the class of topological bases. (Contributed by Chen-Pang He, 9-Oct-2015)

Ref Expression
Assertion onpsstopbas ⊢ On ⊂ TopBases

Proof

Step Hyp Ref Expression
1 onsstopbas ⊢ On ⊆ TopBases
2 indistop ⊢ ∅ ∅ ∈ Top
3 topbas ⊢ ∅ ∅ ∈ Top → ∅ ∅ ∈ TopBases
4 2 3 ax-mp ⊢ ∅ ∅ ∈ TopBases
5 snex ⊢ ∅ ∈ V
6 5 prid2 ⊢ ∅ ∈ ∅ ∅
7 snsn0non ⊢ ¬ ∅ ∈ On
8 jcn ⊢ ∅ ∈ ∅ ∅ → ¬ ∅ ∈ On → ¬ ∅ ∈ ∅ ∅ → ∅ ∈ On
9 6 7 8 mp2 ⊢ ¬ ∅ ∈ ∅ ∅ → ∅ ∈ On
10 onelon ⊢ ∅ ∅ ∈ On ∧ ∅ ∈ ∅ ∅ → ∅ ∈ On
11 10 ex ⊢ ∅ ∅ ∈ On → ∅ ∈ ∅ ∅ → ∅ ∈ On
12 9 11 mto ⊢ ¬ ∅ ∅ ∈ On
13 4 12 pm3.2i ⊢ ∅ ∅ ∈ TopBases ∧ ¬ ∅ ∅ ∈ On
14 ssnelpss ⊢ On ⊆ TopBases → ∅ ∅ ∈ TopBases ∧ ¬ ∅ ∅ ∈ On → On ⊂ TopBases
15 1 13 14 mp2 ⊢ On ⊂ TopBases