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 } )