Theorem snsn0non

Description: The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson ). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj . (Contributed by NM, 21-May-2004) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	snsn0non	$$⊢\neg \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
2	1	snid	$$⊢\left\{\varnothing \right\}\in \left\{\left\{\varnothing \right\}\right\}$$
3	2	n0ii	$$⊢\neg \left\{\left\{\varnothing \right\}\right\}=\varnothing$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	4	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
6	5	n0ii	$$⊢\neg \left\{\varnothing \right\}=\varnothing$$
7		eqcom	$$⊢\varnothing =\left\{\varnothing \right\}\leftrightarrow \left\{\varnothing \right\}=\varnothing$$
8	6 7	mtbir	$$⊢\neg \varnothing =\left\{\varnothing \right\}$$
9	4	elsn	$$⊢\varnothing \in \left\{\left\{\varnothing \right\}\right\}\leftrightarrow \varnothing =\left\{\varnothing \right\}$$
10	8 9	mtbir	$$⊢\neg \varnothing \in \left\{\left\{\varnothing \right\}\right\}$$
11	3 10	pm3.2ni	$$⊢\neg \left(\left\{\left\{\varnothing \right\}\right\}=\varnothing \vee \varnothing \in \left\{\left\{\varnothing \right\}\right\}\right)$$
12		on0eqel	$$⊢\left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}\to \left(\left\{\left\{\varnothing \right\}\right\}=\varnothing \vee \varnothing \in \left\{\left\{\varnothing \right\}\right\}\right)$$
13	11 12	mto	$$⊢\neg \left\{\left\{\varnothing \right\}\right\}\in \mathrm{On}$$