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	⊢ ¬ { 𝐴 } ≈ 2o

Proof

Step	Hyp	Ref	Expression
1		df2o3	⊢ 2o = { ∅ , 1o }
2		0ex	⊢ ∅ ∈ V
3		1oex	⊢ 1o ∈ V
4		1n0	⊢ 1o ≠ ∅
5	4	necomi	⊢ ∅ ≠ 1o
6		prnesn	⊢ ( ( ∅ ∈ V ∧ 1o ∈ V ∧ ∅ ≠ 1o ) → { ∅ , 1o } ≠ { 𝑥 } )
7	2 3 5 6	mp3an	⊢ { ∅ , 1o } ≠ { 𝑥 }
8	1 7	eqnetri	⊢ 2o ≠ { 𝑥 }
9	8	neii	⊢ ¬ 2o = { 𝑥 }
10	9	nex	⊢ ¬ ∃ 𝑥 2o = { 𝑥 }
11		2on0	⊢ 2o ≠ ∅
12		f1cdmsn	⊢ ( ( ◡ 𝑓 : 2o –1-1→ { 𝐴 } ∧ 2o ≠ ∅ ) → ∃ 𝑥 2o = { 𝑥 } )
13	11 12	mpan2	⊢ ( ◡ 𝑓 : 2o –1-1→ { 𝐴 } → ∃ 𝑥 2o = { 𝑥 } )
14	10 13	mto	⊢ ¬ ◡ 𝑓 : 2o –1-1→ { 𝐴 }
15		f1ocnv	⊢ ( 𝑓 : { 𝐴 } –1-1-onto→ 2o → ◡ 𝑓 : 2o –1-1-onto→ { 𝐴 } )
16		f1of1	⊢ ( ◡ 𝑓 : 2o –1-1-onto→ { 𝐴 } → ◡ 𝑓 : 2o –1-1→ { 𝐴 } )
17	15 16	syl	⊢ ( 𝑓 : { 𝐴 } –1-1-onto→ 2o → ◡ 𝑓 : 2o –1-1→ { 𝐴 } )
18	14 17	mto	⊢ ¬ 𝑓 : { 𝐴 } –1-1-onto→ 2o
19	18	nex	⊢ ¬ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ 2o
20		snex	⊢ { 𝐴 } ∈ V
21		2oex	⊢ 2o ∈ V
22		breng	⊢ ( ( { 𝐴 } ∈ V ∧ 2o ∈ V ) → ( { 𝐴 } ≈ 2o ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ 2o ) )
23	20 21 22	mp2an	⊢ ( { 𝐴 } ≈ 2o ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ 2o )
24	19 23	mtbir	⊢ ¬ { 𝐴 } ≈ 2o