Theorem snnen2o

Description: A singleton { A } is never equinumerous with the ordinal number 2. This holds for proper singletons ( A e.V ) as well as for singletons being the empty set ( A e/ V ). (Contributed by AV, 6-Aug-2019)

	Ref	Expression
Assertion	snnen2o	$$⊢\neg \left\{A\right\}\approx 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
2		php5	$$⊢1_{𝑜}\in \mathrm{\omega }\to \neg 1_{𝑜}\approx \mathrm{suc}{1}_{𝑜}$$
3	1 2	ax-mp	$$⊢\neg 1_{𝑜}\approx \mathrm{suc}{1}_{𝑜}$$
4		ensn1g	$$⊢A\in \mathrm{V}\to \left\{A\right\}\approx 1_{𝑜}$$
5		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
6	5	eqcomi	$$⊢\mathrm{suc}{1}_{𝑜}=2_{𝑜}$$
7	6	breq2i	$$⊢1_{𝑜}\approx \mathrm{suc}{1}_{𝑜}\leftrightarrow 1_{𝑜}\approx 2_{𝑜}$$
8		ensymb	$$⊢\left\{A\right\}\approx 1_{𝑜}\leftrightarrow 1_{𝑜}\approx \left\{A\right\}$$
9		entr	$$⊢\left(1_{𝑜}\approx \left\{A\right\}\wedge \left\{A\right\}\approx 2_{𝑜}\right)\to 1_{𝑜}\approx 2_{𝑜}$$
10	9	ex	$$⊢1_{𝑜}\approx \left\{A\right\}\to \left(\left\{A\right\}\approx 2_{𝑜}\to 1_{𝑜}\approx 2_{𝑜}\right)$$
11	8 10	sylbi	$$⊢\left\{A\right\}\approx 1_{𝑜}\to \left(\left\{A\right\}\approx 2_{𝑜}\to 1_{𝑜}\approx 2_{𝑜}\right)$$
12	11	con3rr3	$$⊢\neg 1_{𝑜}\approx 2_{𝑜}\to \left(\left\{A\right\}\approx 1_{𝑜}\to \neg \left\{A\right\}\approx 2_{𝑜}\right)$$
13	7 12	sylnbi	$$⊢\neg 1_{𝑜}\approx \mathrm{suc}{1}_{𝑜}\to \left(\left\{A\right\}\approx 1_{𝑜}\to \neg \left\{A\right\}\approx 2_{𝑜}\right)$$
14	3 4 13	mpsyl	$$⊢A\in \mathrm{V}\to \neg \left\{A\right\}\approx 2_{𝑜}$$
15		2on0	$$⊢2_{𝑜}\ne \varnothing$$
16		ensymb	$$⊢\varnothing \approx 2_{𝑜}\leftrightarrow 2_{𝑜}\approx \varnothing$$
17		en0	$$⊢2_{𝑜}\approx \varnothing \leftrightarrow 2_{𝑜}=\varnothing$$
18	16 17	bitri	$$⊢\varnothing \approx 2_{𝑜}\leftrightarrow 2_{𝑜}=\varnothing$$
19	15 18	nemtbir	$$⊢\neg \varnothing \approx 2_{𝑜}$$
20		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
21	20	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
22	21	breq1d	$$⊢\neg A\in \mathrm{V}\to \left(\left\{A\right\}\approx 2_{𝑜}\leftrightarrow \varnothing \approx 2_{𝑜}\right)$$
23	19 22	mtbiri	$$⊢\neg A\in \mathrm{V}\to \neg \left\{A\right\}\approx 2_{𝑜}$$
24	14 23	pm2.61i	$$⊢\neg \left\{A\right\}\approx 2_{𝑜}$$