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 |
|
snex |
|- { x } e. _V |
5 |
|
eqsbc3 |
|- ( { 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
|
abeq2i |
|- ( 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
|
syl6bb |
|- ( ( 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 |