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

Metamath Proof Explorer

Theorem en1b

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015) Avoid ax-un . (Revised by BTernaryTau, 24-Sep-2024)

Ref Expression
Assertion en1b 
|- ( A ~~ 1o <-> A = { U. A } )

Proof

Step Hyp Ref Expression
1 en1 
 |-  ( A ~~ 1o <-> E. x A = { x } )
2 id 
 |-  ( A = { x } -> A = { x } )
3 unieq 
 |-  ( A = { x } -> U. A = U. { x } )
4 unisnv 
 |-  U. { x } = x
5 3 4 eqtrdi 
 |-  ( A = { x } -> U. A = x )
6 5 sneqd 
 |-  ( A = { x } -> { U. A } = { x } )
7 2 6 eqtr4d 
 |-  ( A = { x } -> A = { U. A } )
8 7 exlimiv 
 |-  ( E. x A = { x } -> A = { U. A } )
9 1 8 sylbi 
 |-  ( A ~~ 1o -> A = { U. A } )
10 id 
 |-  ( A = { U. A } -> A = { U. A } )
11 eqsnuniex 
 |-  ( A = { U. A } -> U. A e. _V )
12 ensn1g 
 |-  ( U. A e. _V -> { U. A } ~~ 1o )
13 11 12 syl 
 |-  ( A = { U. A } -> { U. A } ~~ 1o )
14 10 13 eqbrtrd 
 |-  ( A = { U. A } -> A ~~ 1o )
15 9 14 impbii 
 |-  ( A ~~ 1o <-> A = { U. A } )