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