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

Metamath Proof Explorer

Theorem en1

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004) Avoid ax-un . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Assertion en1 
|- ( A ~~ 1o <-> E. x A = { x } )

Proof

Step Hyp Ref Expression
1 df1o2 
 |-  1o = { (/) }
2 1 breq2i 
 |-  ( A ~~ 1o <-> A ~~ { (/) } )
3 encv 
 |-  ( A ~~ { (/) } -> ( A e. _V /\ { (/) } e. _V ) )
4 breng 
 |-  ( ( A e. _V /\ { (/) } e. _V ) -> ( A ~~ { (/) } <-> E. f f : A -1-1-onto-> { (/) } ) )
5 3 4 syl 
 |-  ( A ~~ { (/) } -> ( A ~~ { (/) } <-> E. f f : A -1-1-onto-> { (/) } ) )
6 5 ibi 
 |-  ( A ~~ { (/) } -> E. f f : A -1-1-onto-> { (/) } )
7 2 6 sylbi 
 |-  ( A ~~ 1o -> E. f f : A -1-1-onto-> { (/) } )
8 f1ocnv 
 |-  ( f : A -1-1-onto-> { (/) } -> `' f : { (/) } -1-1-onto-> A )
9 f1ofo 
 |-  ( `' f : { (/) } -1-1-onto-> A -> `' f : { (/) } -onto-> A )
10 forn 
 |-  ( `' f : { (/) } -onto-> A -> ran `' f = A )
11 9 10 syl 
 |-  ( `' f : { (/) } -1-1-onto-> A -> ran `' f = A )
12 f1of 
 |-  ( `' f : { (/) } -1-1-onto-> A -> `' f : { (/) } --> A )
13 0ex 
 |-  (/) e. _V
14 13 fsn2 
 |-  ( `' f : { (/) } --> A <-> ( ( `' f ` (/) ) e. A /\ `' f = { <. (/) , ( `' f ` (/) ) >. } ) )
15 14 simprbi 
 |-  ( `' f : { (/) } --> A -> `' f = { <. (/) , ( `' f ` (/) ) >. } )
16 12 15 syl 
 |-  ( `' f : { (/) } -1-1-onto-> A -> `' f = { <. (/) , ( `' f ` (/) ) >. } )
17 16 rneqd 
 |-  ( `' f : { (/) } -1-1-onto-> A -> ran `' f = ran { <. (/) , ( `' f ` (/) ) >. } )
18 13 rnsnop 
 |-  ran { <. (/) , ( `' f ` (/) ) >. } = { ( `' f ` (/) ) }
19 17 18 eqtrdi 
 |-  ( `' f : { (/) } -1-1-onto-> A -> ran `' f = { ( `' f ` (/) ) } )
20 11 19 eqtr3d 
 |-  ( `' f : { (/) } -1-1-onto-> A -> A = { ( `' f ` (/) ) } )
21 fvex 
 |-  ( `' f ` (/) ) e. _V
22 sneq 
 |-  ( x = ( `' f ` (/) ) -> { x } = { ( `' f ` (/) ) } )
23 22 eqeq2d 
 |-  ( x = ( `' f ` (/) ) -> ( A = { x } <-> A = { ( `' f ` (/) ) } ) )
24 21 23 spcev 
 |-  ( A = { ( `' f ` (/) ) } -> E. x A = { x } )
25 8 20 24 3syl 
 |-  ( f : A -1-1-onto-> { (/) } -> E. x A = { x } )
26 25 exlimiv 
 |-  ( E. f f : A -1-1-onto-> { (/) } -> E. x A = { x } )
27 7 26 syl 
 |-  ( A ~~ 1o -> E. x A = { x } )
28 vex 
 |-  x e. _V
29 28 ensn1 
 |-  { x } ~~ 1o
30 breq1 
 |-  ( A = { x } -> ( A ~~ 1o <-> { x } ~~ 1o ) )
31 29 30 mpbiri 
 |-  ( A = { x } -> A ~~ 1o )
32 31 exlimiv 
 |-  ( E. x A = { x } -> A ~~ 1o )
33 27 32 impbii 
 |-  ( A ~~ 1o <-> E. x A = { x } )