Metamath Proof Explorer

Theorem en1OLD

Description: Obsolete version of en1 as of 23-Sep-2024. (Contributed by NM, 25-Jul-2004) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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