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	$$⊢\mathrm{On}\subset \mathrm{TopBases}$$

Proof

Step	Hyp	Ref	Expression
1		onsstopbas	$$⊢\mathrm{On}\subseteq \mathrm{TopBases}$$
2		indistop	$$⊢\left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{Top}$$
3		topbas	$$⊢\left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{Top}\to \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{TopBases}$$
4	2 3	ax-mp	$$⊢\left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{TopBases}$$
5		snex	$$⊢\left\{\left\{\varnothing \right\}\right\}\in \mathrm{V}$$
6	5	prid2	$$⊢\left\{\left\{\varnothing \right\}\right\}\in \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}$$
7		snsn0non	$$⊢\neg \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}$$
8		jcn	$$⊢\left\{\left\{\varnothing \right\}\right\}\in \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\to \left(\neg \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}\to \neg \left(\left\{\left\{\varnothing \right\}\right\}\in \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\to \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}\right)\right)$$
9	6 7 8	mp2	$$⊢\neg \left(\left\{\left\{\varnothing \right\}\right\}\in \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\to \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}\right)$$
10		onelon	$$⊢\left(\left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{On}\wedge \left\{\left\{\varnothing \right\}\right\}\in \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\right)\to \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}$$
11	10	ex	$$⊢\left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{On}\to \left(\left\{\left\{\varnothing \right\}\right\}\in \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\to \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}\right)$$
12	9 11	mto	$$⊢\neg \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{On}$$
13	4 12	pm3.2i	$$⊢\left(\left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{TopBases}\wedge \neg \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{On}\right)$$
14		ssnelpss	$$⊢\mathrm{On}\subseteq \mathrm{TopBases}\to \left(\left(\left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{TopBases}\wedge \neg \left\{\varnothing ,\left\{\left\{\varnothing \right\}\right\}\right\}\in \mathrm{On}\right)\to \mathrm{On}\subset \mathrm{TopBases}\right)$$
15	1 13 14	mp2	$$⊢\mathrm{On}\subset \mathrm{TopBases}$$