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

Proof

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

Metamath Proof Explorer

Theorem snnen2o

Proof