Step |
Hyp |
Ref |
Expression |
1 |
|
negiso.1 |
|- F = ( x e. RR |-> -u x ) |
2 |
|
simpr |
|- ( ( T. /\ x e. RR ) -> x e. RR ) |
3 |
2
|
renegcld |
|- ( ( T. /\ x e. RR ) -> -u x e. RR ) |
4 |
|
simpr |
|- ( ( T. /\ y e. RR ) -> y e. RR ) |
5 |
4
|
renegcld |
|- ( ( T. /\ y e. RR ) -> -u y e. RR ) |
6 |
|
recn |
|- ( x e. RR -> x e. CC ) |
7 |
|
recn |
|- ( y e. RR -> y e. CC ) |
8 |
|
negcon2 |
|- ( ( x e. CC /\ y e. CC ) -> ( x = -u y <-> y = -u x ) ) |
9 |
6 7 8
|
syl2an |
|- ( ( x e. RR /\ y e. RR ) -> ( x = -u y <-> y = -u x ) ) |
10 |
9
|
adantl |
|- ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( x = -u y <-> y = -u x ) ) |
11 |
1 3 5 10
|
f1ocnv2d |
|- ( T. -> ( F : RR -1-1-onto-> RR /\ `' F = ( y e. RR |-> -u y ) ) ) |
12 |
11
|
mptru |
|- ( F : RR -1-1-onto-> RR /\ `' F = ( y e. RR |-> -u y ) ) |
13 |
12
|
simpli |
|- F : RR -1-1-onto-> RR |
14 |
|
ltneg |
|- ( ( z e. RR /\ y e. RR ) -> ( z < y <-> -u y < -u z ) ) |
15 |
|
negex |
|- -u z e. _V |
16 |
|
negex |
|- -u y e. _V |
17 |
15 16
|
brcnv |
|- ( -u z `' < -u y <-> -u y < -u z ) |
18 |
14 17
|
bitr4di |
|- ( ( z e. RR /\ y e. RR ) -> ( z < y <-> -u z `' < -u y ) ) |
19 |
|
negeq |
|- ( x = z -> -u x = -u z ) |
20 |
19 1 15
|
fvmpt |
|- ( z e. RR -> ( F ` z ) = -u z ) |
21 |
|
negeq |
|- ( x = y -> -u x = -u y ) |
22 |
21 1 16
|
fvmpt |
|- ( y e. RR -> ( F ` y ) = -u y ) |
23 |
20 22
|
breqan12d |
|- ( ( z e. RR /\ y e. RR ) -> ( ( F ` z ) `' < ( F ` y ) <-> -u z `' < -u y ) ) |
24 |
18 23
|
bitr4d |
|- ( ( z e. RR /\ y e. RR ) -> ( z < y <-> ( F ` z ) `' < ( F ` y ) ) ) |
25 |
24
|
rgen2 |
|- A. z e. RR A. y e. RR ( z < y <-> ( F ` z ) `' < ( F ` y ) ) |
26 |
|
df-isom |
|- ( F Isom < , `' < ( RR , RR ) <-> ( F : RR -1-1-onto-> RR /\ A. z e. RR A. y e. RR ( z < y <-> ( F ` z ) `' < ( F ` y ) ) ) ) |
27 |
13 25 26
|
mpbir2an |
|- F Isom < , `' < ( RR , RR ) |
28 |
|
negeq |
|- ( y = x -> -u y = -u x ) |
29 |
28
|
cbvmptv |
|- ( y e. RR |-> -u y ) = ( x e. RR |-> -u x ) |
30 |
12
|
simpri |
|- `' F = ( y e. RR |-> -u y ) |
31 |
29 30 1
|
3eqtr4i |
|- `' F = F |
32 |
27 31
|
pm3.2i |
|- ( F Isom < , `' < ( RR , RR ) /\ `' F = F ) |