Metamath Proof Explorer

Theorem f1omptsnlem

Description: This is the core of the proof of f1omptsn , but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020)

Ref Expression
Hypotheses f1omptsn.f 
|- F = ( x e. A |-> { x } )
f1omptsn.r 
|- R = { u | E. x e. A u = { x } }
Assertion f1omptsnlem 
|- F : A -1-1-onto-> R

Proof

Step Hyp Ref Expression
1 f1omptsn.f 
 |-  F = ( x e. A |-> { x } )
2 f1omptsn.r 
 |-  R = { u | E. x e. A u = { x } }
3 eqid 
 |-  { x } = { x }
4 vsnex 
 |-  { x } e. _V
5 eqsbc1 
 |-  ( { x } e. _V -> ( [. { x } / u ]. u = { x } <-> { x } = { x } ) )
6 4 5 ax-mp 
 |-  ( [. { x } / u ]. u = { x } <-> { x } = { x } )
7 3 6 mpbir 
 |-  [. { x } / u ]. u = { x }
8 sbcel2 
 |-  ( [. { x } / u ]. x e. A <-> x e. [_ { x } / u ]_ A )
9 csbconstg 
 |-  ( { x } e. _V -> [_ { x } / u ]_ A = A )
10 4 9 ax-mp 
 |-  [_ { x } / u ]_ A = A
11 10 eleq2i 
 |-  ( x e. [_ { x } / u ]_ A <-> x e. A )
12 8 11 bitri 
 |-  ( [. { x } / u ]. x e. A <-> x e. A )
13 2 eqabri 
 |-  ( u e. R <-> E. x e. A u = { x } )
14 df-rex 
 |-  ( E. x e. A u = { x } <-> E. x ( x e. A /\ u = { x } ) )
15 13 14 sylbbr 
 |-  ( E. x ( x e. A /\ u = { x } ) -> u e. R )
16 15 19.23bi 
 |-  ( ( x e. A /\ u = { x } ) -> u e. R )
17 16 sbcth 
 |-  ( { x } e. _V -> [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R ) )
18 4 17 ax-mp 
 |-  [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R )
19 sbcimg 
 |-  ( { x } e. _V -> ( [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R ) <-> ( [. { x } / u ]. ( x e. A /\ u = { x } ) -> [. { x } / u ]. u e. R ) ) )
20 4 19 ax-mp 
 |-  ( [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R ) <-> ( [. { x } / u ]. ( x e. A /\ u = { x } ) -> [. { x } / u ]. u e. R ) )
21 18 20 mpbi 
 |-  ( [. { x } / u ]. ( x e. A /\ u = { x } ) -> [. { x } / u ]. u e. R )
22 sbcan 
 |-  ( [. { x } / u ]. ( x e. A /\ u = { x } ) <-> ( [. { x } / u ]. x e. A /\ [. { x } / u ]. u = { x } ) )
23 sbcel1v 
 |-  ( [. { x } / u ]. u e. R <-> { x } e. R )
24 21 22 23 3imtr3i 
 |-  ( ( [. { x } / u ]. x e. A /\ [. { x } / u ]. u = { x } ) -> { x } e. R )
25 12 24 sylanbr 
 |-  ( ( x e. A /\ [. { x } / u ]. u = { x } ) -> { x } e. R )
26 7 25 mpan2 
 |-  ( x e. A -> { x } e. R )
27 1 26 fmpti 
 |-  F : A --> R
28 1 fvmpt2 
 |-  ( ( x e. A /\ { x } e. R ) -> ( F ` x ) = { x } )
29 26 28 mpdan 
 |-  ( x e. A -> ( F ` x ) = { x } )
30 sneq 
 |-  ( x = y -> { x } = { y } )
31 30 1 4 fvmpt3i 
 |-  ( y e. A -> ( F ` y ) = { y } )
32 29 31 eqeqan12d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) <-> { x } = { y } ) )
33 vex 
 |-  x e. _V
34 sneqbg 
 |-  ( x e. _V -> ( { x } = { y } <-> x = y ) )
35 33 34 ax-mp 
 |-  ( { x } = { y } <-> x = y )
36 32 35 bitrdi 
 |-  ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
37 36 biimpd 
 |-  ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
38 37 rgen2 
 |-  A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y )
39 dff13 
 |-  ( F : A -1-1-> R <-> ( F : A --> R /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
40 27 38 39 mpbir2an 
 |-  F : A -1-1-> R
41 f1f1orn 
 |-  ( F : A -1-1-> R -> F : A -1-1-onto-> ran F )
42 40 41 ax-mp 
 |-  F : A -1-1-onto-> ran F
43 rnmptsn 
 |-  ran ( x e. A |-> { x } ) = { u | E. x e. A u = { x } }
44 1 rneqi 
 |-  ran F = ran ( x e. A |-> { x } )
45 43 44 2 3eqtr4i 
 |-  ran F = R
46 f1oeq3 
 |-  ( ran F = R -> ( F : A -1-1-onto-> ran F <-> F : A -1-1-onto-> R ) )
47 45 46 ax-mp 
 |-  ( F : A -1-1-onto-> ran F <-> F : A -1-1-onto-> R )
48 42 47 mpbi 
 |-  F : A -1-1-onto-> R