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