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

Metamath Proof Explorer

Theorem ensn1

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002) Avoid ax-un . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Hypothesis ensn1.1 
|- A e. _V
Assertion ensn1 
|- { A } ~~ 1o

Proof

Step Hyp Ref Expression
1 ensn1.1 
 |-  A e. _V
2 snex 
 |-  { <. A , (/) >. } e. _V
3 f1oeq1 
 |-  ( f = { <. A , (/) >. } -> ( f : { A } -1-1-onto-> { (/) } <-> { <. A , (/) >. } : { A } -1-1-onto-> { (/) } ) )
4 0ex 
 |-  (/) e. _V
5 1 4 f1osn 
 |-  { <. A , (/) >. } : { A } -1-1-onto-> { (/) }
6 2 3 5 ceqsexv2d 
 |-  E. f f : { A } -1-1-onto-> { (/) }
7 snex 
 |-  { A } e. _V
8 snex 
 |-  { (/) } e. _V
9 breng 
 |-  ( ( { A } e. _V /\ { (/) } e. _V ) -> ( { A } ~~ { (/) } <-> E. f f : { A } -1-1-onto-> { (/) } ) )
10 7 8 9 mp2an 
 |-  ( { A } ~~ { (/) } <-> E. f f : { A } -1-1-onto-> { (/) } )
11 6 10 mpbir 
 |-  { A } ~~ { (/) }
12 df1o2 
 |-  1o = { (/) }
13 11 12 breqtrri 
 |-  { A } ~~ 1o