This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- -. { A } ~~ 2o

Proof

Step Hyp Ref Expression
1 df2o3 
 |-  2o = { (/) , 1o }
2 0ex 
 |-  (/) e. _V
3 1oex 
 |-  1o e. _V
4 1n0 
 |-  1o =/= (/)
5 4 necomi 
 |-  (/) =/= 1o
6 prnesn 
 |-  ( ( (/) e. _V /\ 1o e. _V /\ (/) =/= 1o ) -> { (/) , 1o } =/= { x } )
7 2 3 5 6 mp3an 
 |-  { (/) , 1o } =/= { x }
8 1 7 eqnetri 
 |-  2o =/= { x }
9 8 neii 
 |-  -. 2o = { x }
10 9 nex 
 |-  -. E. x 2o = { x }
11 2on0 
 |-  2o =/= (/)
12 f1cdmsn 
 |-  ( ( `' f : 2o -1-1-> { A } /\ 2o =/= (/) ) -> E. x 2o = { x } )
13 11 12 mpan2 
 |-  ( `' f : 2o -1-1-> { A } -> E. x 2o = { x } )
14 10 13 mto 
 |-  -. `' f : 2o -1-1-> { A }
15 f1ocnv 
 |-  ( f : { A } -1-1-onto-> 2o -> `' f : 2o -1-1-onto-> { A } )
16 f1of1 
 |-  ( `' f : 2o -1-1-onto-> { A } -> `' f : 2o -1-1-> { A } )
17 15 16 syl 
 |-  ( f : { A } -1-1-onto-> 2o -> `' f : 2o -1-1-> { A } )
18 14 17 mto 
 |-  -. f : { A } -1-1-onto-> 2o
19 18 nex 
 |-  -. E. f f : { A } -1-1-onto-> 2o
20 snex 
 |-  { A } e. _V
21 2oex 
 |-  2o e. _V
22 breng 
 |-  ( ( { A } e. _V /\ 2o e. _V ) -> ( { A } ~~ 2o <-> E. f f : { A } -1-1-onto-> 2o ) )
23 20 21 22 mp2an 
 |-  ( { A } ~~ 2o <-> E. f f : { A } -1-1-onto-> 2o )
24 19 23 mtbir 
 |-  -. { A } ~~ 2o