Step |
Hyp |
Ref |
Expression |
1 |
|
eff |
|- exp : CC --> CC |
2 |
|
ffn |
|- ( exp : CC --> CC -> exp Fn CC ) |
3 |
1 2
|
ax-mp |
|- exp Fn CC |
4 |
|
ax-resscn |
|- RR C_ CC |
5 |
|
fnssres |
|- ( ( exp Fn CC /\ RR C_ CC ) -> ( exp |` RR ) Fn RR ) |
6 |
3 4 5
|
mp2an |
|- ( exp |` RR ) Fn RR |
7 |
|
fvres |
|- ( x e. RR -> ( ( exp |` RR ) ` x ) = ( exp ` x ) ) |
8 |
|
rpefcl |
|- ( x e. RR -> ( exp ` x ) e. RR+ ) |
9 |
7 8
|
eqeltrd |
|- ( x e. RR -> ( ( exp |` RR ) ` x ) e. RR+ ) |
10 |
9
|
rgen |
|- A. x e. RR ( ( exp |` RR ) ` x ) e. RR+ |
11 |
|
ffnfv |
|- ( ( exp |` RR ) : RR --> RR+ <-> ( ( exp |` RR ) Fn RR /\ A. x e. RR ( ( exp |` RR ) ` x ) e. RR+ ) ) |
12 |
6 10 11
|
mpbir2an |
|- ( exp |` RR ) : RR --> RR+ |
13 |
|
fvres |
|- ( y e. RR -> ( ( exp |` RR ) ` y ) = ( exp ` y ) ) |
14 |
7 13
|
eqeqan12d |
|- ( ( x e. RR /\ y e. RR ) -> ( ( ( exp |` RR ) ` x ) = ( ( exp |` RR ) ` y ) <-> ( exp ` x ) = ( exp ` y ) ) ) |
15 |
|
reef11 |
|- ( ( x e. RR /\ y e. RR ) -> ( ( exp ` x ) = ( exp ` y ) <-> x = y ) ) |
16 |
15
|
biimpd |
|- ( ( x e. RR /\ y e. RR ) -> ( ( exp ` x ) = ( exp ` y ) -> x = y ) ) |
17 |
14 16
|
sylbid |
|- ( ( x e. RR /\ y e. RR ) -> ( ( ( exp |` RR ) ` x ) = ( ( exp |` RR ) ` y ) -> x = y ) ) |
18 |
17
|
rgen2 |
|- A. x e. RR A. y e. RR ( ( ( exp |` RR ) ` x ) = ( ( exp |` RR ) ` y ) -> x = y ) |
19 |
|
dff13 |
|- ( ( exp |` RR ) : RR -1-1-> RR+ <-> ( ( exp |` RR ) : RR --> RR+ /\ A. x e. RR A. y e. RR ( ( ( exp |` RR ) ` x ) = ( ( exp |` RR ) ` y ) -> x = y ) ) ) |
20 |
12 18 19
|
mpbir2an |
|- ( exp |` RR ) : RR -1-1-> RR+ |