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 C. TopBases

Proof

Step	Hyp	Ref	Expression
1		onsstopbas	|- On C_ TopBases
2		indistop	|- { (/) , { { (/) } } } e. Top
3		topbas	|- ( { (/) , { { (/) } } } e. Top -> { (/) , { { (/) } } } e. TopBases )
4	2 3	ax-mp	|- { (/) , { { (/) } } } e. TopBases
5		snex	|- { { (/) } } e. _V
6	5	prid2	|- { { (/) } } e. { (/) , { { (/) } } }
7		snsn0non	|- -. { { (/) } } e. On
8		jcn	|- ( { { (/) } } e. { (/) , { { (/) } } } -> ( -. { { (/) } } e. On -> -. ( { { (/) } } e. { (/) , { { (/) } } } -> { { (/) } } e. On ) ) )
9	6 7 8	mp2	|- -. ( { { (/) } } e. { (/) , { { (/) } } } -> { { (/) } } e. On )
10		onelon	|- ( ( { (/) , { { (/) } } } e. On /\ { { (/) } } e. { (/) , { { (/) } } } ) -> { { (/) } } e. On )
11	10	ex	|- ( { (/) , { { (/) } } } e. On -> ( { { (/) } } e. { (/) , { { (/) } } } -> { { (/) } } e. On ) )
12	9 11	mto	|- -. { (/) , { { (/) } } } e. On
13	4 12	pm3.2i	|- ( { (/) , { { (/) } } } e. TopBases /\ -. { (/) , { { (/) } } } e. On )
14		ssnelpss	|- ( On C_ TopBases -> ( ( { (/) , { { (/) } } } e. TopBases /\ -. { (/) , { { (/) } } } e. On ) -> On C. TopBases ) )
15	1 13 14	mp2	|- On C. TopBases