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) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 1-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
4		1n0	$$⊢1_{𝑜}\ne \varnothing$$
5	4	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
6		prnesn	$$⊢\left(\varnothing \in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{V}\wedge \varnothing \ne 1_{𝑜}\right)\to \left\{\varnothing ,1_{𝑜}\right\}\ne \left\{x\right\}$$
7	2 3 5 6	mp3an	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\ne \left\{x\right\}$$
8	1 7	eqnetri	$$⊢2_{𝑜}\ne \left\{x\right\}$$
9	8	neii	$$⊢\neg 2_{𝑜}=\left\{x\right\}$$
10	9	nex	$$⊢\neg \exists x{2}_{𝑜}=\left\{x\right\}$$
11		2on0	$$⊢2_{𝑜}\ne \varnothing$$
12		f1cdmsn	$$⊢\left(f^{-1}:2_{𝑜}\underset{1-1}{⟶}\left\{A\right\}\wedge 2_{𝑜}\ne \varnothing \right)\to \exists x{2}_{𝑜}=\left\{x\right\}$$
13	11 12	mpan2	$$⊢f^{-1}:2_{𝑜}\underset{1-1}{⟶}\left\{A\right\}\to \exists x{2}_{𝑜}=\left\{x\right\}$$
14	10 13	mto	$$⊢\neg f^{-1}:2_{𝑜}\underset{1-1}{⟶}\left\{A\right\}$$
15		f1ocnv	$$⊢f:\left\{A\right\}\underset{1-1\; onto}{⟶}{2}_{𝑜}\to f^{-1}:2_{𝑜}\underset{1-1\; onto}{⟶}\left\{A\right\}$$
16		f1of1	$$⊢f^{-1}:2_{𝑜}\underset{1-1\; onto}{⟶}\left\{A\right\}\to f^{-1}:2_{𝑜}\underset{1-1}{⟶}\left\{A\right\}$$
17	15 16	syl	$$⊢f:\left\{A\right\}\underset{1-1\; onto}{⟶}{2}_{𝑜}\to f^{-1}:2_{𝑜}\underset{1-1}{⟶}\left\{A\right\}$$
18	14 17	mto	$$⊢\neg f:\left\{A\right\}\underset{1-1\; onto}{⟶}{2}_{𝑜}$$
19	18	nex	$$⊢\neg \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}{2}_{𝑜}$$
20		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
21		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
22		breng	$$⊢\left(\left\{A\right\}\in \mathrm{V}\wedge 2_{𝑜}\in \mathrm{V}\right)\to \left(\left\{A\right\}\approx 2_{𝑜}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}{2}_{𝑜}\right)$$
23	20 21 22	mp2an	$$⊢\left\{A\right\}\approx 2_{𝑜}\leftrightarrow \exists ff:\left\{A\right\}\underset{1-1\; onto}{⟶}{2}_{𝑜}$$
24	19 23	mtbir	$$⊢\neg \left\{A\right\}\approx 2_{𝑜}$$