Metamath Proof Explorer


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 ( ( 𝑓 : 2o1-1→ { 𝐴 } ∧ 2o ≠ ∅ ) → ∃ 𝑥 2o = { 𝑥 } )
13 11 12 mpan2 ( 𝑓 : 2o1-1→ { 𝐴 } → ∃ 𝑥 2o = { 𝑥 } )
14 10 13 mto ¬ 𝑓 : 2o1-1→ { 𝐴 }
15 f1ocnv ( 𝑓 : { 𝐴 } –1-1-onto→ 2o 𝑓 : 2o1-1-onto→ { 𝐴 } )
16 f1of1 ( 𝑓 : 2o1-1-onto→ { 𝐴 } → 𝑓 : 2o1-1→ { 𝐴 } )
17 15 16 syl ( 𝑓 : { 𝐴 } –1-1-onto→ 2o 𝑓 : 2o1-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