Metamath Proof Explorer

Theorem xrhmeo

Description: The bijection from [ -u 1 , 1 ] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses xrhmeo.f 
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
xrhmeo.g 
|- G = ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
xrhmeo.j 
|- J = ( TopOpen ` CCfld )
Assertion xrhmeo 
|- ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) /\ G e. ( ( J |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) )

Proof

Step Hyp Ref Expression
1 xrhmeo.f 
 |-  F = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
2 xrhmeo.g 
 |-  G = ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
3 xrhmeo.j 
 |-  J = ( TopOpen ` CCfld )
4 iccssxr 
 |-  ( -u 1 [,] 1 ) C_ RR*
5 xrltso 
 |-  < Or RR*
6 soss 
 |-  ( ( -u 1 [,] 1 ) C_ RR* -> ( < Or RR* -> < Or ( -u 1 [,] 1 ) ) )
7 4 5 6 mp2 
 |-  < Or ( -u 1 [,] 1 )
8 sopo 
 |-  ( < Or RR* -> < Po RR* )
9 5 8 ax-mp 
 |-  < Po RR*
10 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
11 neg1rr 
 |-  -u 1 e. RR
12 1re 
 |-  1 e. RR
13 11 12 elicc2i 
 |-  ( y e. ( -u 1 [,] 1 ) <-> ( y e. RR /\ -u 1 <_ y /\ y <_ 1 ) )
14 13 simp1bi 
 |-  ( y e. ( -u 1 [,] 1 ) -> y e. RR )
15 14 adantr 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> y e. RR )
16 simpr 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> 0 <_ y )
17 13 simp3bi 
 |-  ( y e. ( -u 1 [,] 1 ) -> y <_ 1 )
18 17 adantr 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> y <_ 1 )
19 elicc01 
 |-  ( y e. ( 0 [,] 1 ) <-> ( y e. RR /\ 0 <_ y /\ y <_ 1 ) )
20 15 16 18 19 syl3anbrc 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> y e. ( 0 [,] 1 ) )
21 1 iccpnfcnv 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( v e. ( 0 [,] +oo ) |-> if ( v = +oo , 1 , ( v / ( 1 + v ) ) ) ) )
22 21 simpli 
 |-  F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )
23 f1of 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> F : ( 0 [,] 1 ) --> ( 0 [,] +oo ) )
24 22 23 ax-mp 
 |-  F : ( 0 [,] 1 ) --> ( 0 [,] +oo )
25 24 ffvelrni 
 |-  ( y e. ( 0 [,] 1 ) -> ( F ` y ) e. ( 0 [,] +oo ) )
26 20 25 syl 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> ( F ` y ) e. ( 0 [,] +oo ) )
27 10 26 sseldi 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> ( F ` y ) e. RR* )
28 14 adantr 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> y e. RR )
29 28 renegcld 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u y e. RR )
30 0re 
 |-  0 e. RR
31 letric 
 |-  ( ( 0 e. RR /\ y e. RR ) -> ( 0 <_ y \/ y <_ 0 ) )
32 30 14 31 sylancr 
 |-  ( y e. ( -u 1 [,] 1 ) -> ( 0 <_ y \/ y <_ 0 ) )
33 32 orcanai 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> y <_ 0 )
34 28 le0neg1d 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( y <_ 0 <-> 0 <_ -u y ) )
35 33 34 mpbid 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> 0 <_ -u y )
36 13 simp2bi 
 |-  ( y e. ( -u 1 [,] 1 ) -> -u 1 <_ y )
37 36 adantr 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u 1 <_ y )
38 lenegcon1 
 |-  ( ( 1 e. RR /\ y e. RR ) -> ( -u 1 <_ y <-> -u y <_ 1 ) )
39 12 28 38 sylancr 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( -u 1 <_ y <-> -u y <_ 1 ) )
40 37 39 mpbid 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u y <_ 1 )
41 elicc01 
 |-  ( -u y e. ( 0 [,] 1 ) <-> ( -u y e. RR /\ 0 <_ -u y /\ -u y <_ 1 ) )
42 29 35 40 41 syl3anbrc 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u y e. ( 0 [,] 1 ) )
43 24 ffvelrni 
 |-  ( -u y e. ( 0 [,] 1 ) -> ( F ` -u y ) e. ( 0 [,] +oo ) )
44 42 43 syl 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( F ` -u y ) e. ( 0 [,] +oo ) )
45 10 44 sseldi 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( F ` -u y ) e. RR* )
46 45 xnegcld 
 |-  ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -e ( F ` -u y ) e. RR* )
47 27 46 ifclda 
 |-  ( y e. ( -u 1 [,] 1 ) -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) e. RR* )
48 2 47 fmpti 
 |-  G : ( -u 1 [,] 1 ) --> RR*
49 frn 
 |-  ( G : ( -u 1 [,] 1 ) --> RR* -> ran G C_ RR* )
50 48 49 ax-mp 
 |-  ran G C_ RR*
51 ssabral 
 |-  ( RR* C_ { z | E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) } <-> A. z e. RR* E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
52 0le1 
 |-  0 <_ 1
53 le0neg2 
 |-  ( 1 e. RR -> ( 0 <_ 1 <-> -u 1 <_ 0 ) )
54 12 53 ax-mp 
 |-  ( 0 <_ 1 <-> -u 1 <_ 0 )
55 52 54 mpbi 
 |-  -u 1 <_ 0
56 1le1 
 |-  1 <_ 1
57 iccss 
 |-  ( ( ( -u 1 e. RR /\ 1 e. RR ) /\ ( -u 1 <_ 0 /\ 1 <_ 1 ) ) -> ( 0 [,] 1 ) C_ ( -u 1 [,] 1 ) )
58 11 12 55 56 57 mp4an 
 |-  ( 0 [,] 1 ) C_ ( -u 1 [,] 1 )
59 elxrge0 
 |-  ( z e. ( 0 [,] +oo ) <-> ( z e. RR* /\ 0 <_ z ) )
60 f1ocnv 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> `' F : ( 0 [,] +oo ) -1-1-onto-> ( 0 [,] 1 ) )
61 f1of 
 |-  ( `' F : ( 0 [,] +oo ) -1-1-onto-> ( 0 [,] 1 ) -> `' F : ( 0 [,] +oo ) --> ( 0 [,] 1 ) )
62 22 60 61 mp2b 
 |-  `' F : ( 0 [,] +oo ) --> ( 0 [,] 1 )
63 62 ffvelrni 
 |-  ( z e. ( 0 [,] +oo ) -> ( `' F ` z ) e. ( 0 [,] 1 ) )
64 59 63 sylbir 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> ( `' F ` z ) e. ( 0 [,] 1 ) )
65 58 64 sseldi 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> ( `' F ` z ) e. ( -u 1 [,] 1 ) )
66 elicc01 
 |-  ( ( `' F ` z ) e. ( 0 [,] 1 ) <-> ( ( `' F ` z ) e. RR /\ 0 <_ ( `' F ` z ) /\ ( `' F ` z ) <_ 1 ) )
67 66 simp2bi 
 |-  ( ( `' F ` z ) e. ( 0 [,] 1 ) -> 0 <_ ( `' F ` z ) )
68 64 67 syl 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> 0 <_ ( `' F ` z ) )
69 59 biimpri 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> z e. ( 0 [,] +oo ) )
70 f1ocnvfv2 
 |-  ( ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ z e. ( 0 [,] +oo ) ) -> ( F ` ( `' F ` z ) ) = z )
71 22 69 70 sylancr 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> ( F ` ( `' F ` z ) ) = z )
72 71 eqcomd 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> z = ( F ` ( `' F ` z ) ) )
73 breq2 
 |-  ( y = ( `' F ` z ) -> ( 0 <_ y <-> 0 <_ ( `' F ` z ) ) )
74 fveq2 
 |-  ( y = ( `' F ` z ) -> ( F ` y ) = ( F ` ( `' F ` z ) ) )
75 74 eqeq2d 
 |-  ( y = ( `' F ` z ) -> ( z = ( F ` y ) <-> z = ( F ` ( `' F ` z ) ) ) )
76 73 75 anbi12d 
 |-  ( y = ( `' F ` z ) -> ( ( 0 <_ y /\ z = ( F ` y ) ) <-> ( 0 <_ ( `' F ` z ) /\ z = ( F ` ( `' F ` z ) ) ) ) )
77 76 rspcev 
 |-  ( ( ( `' F ` z ) e. ( -u 1 [,] 1 ) /\ ( 0 <_ ( `' F ` z ) /\ z = ( F ` ( `' F ` z ) ) ) ) -> E. y e. ( -u 1 [,] 1 ) ( 0 <_ y /\ z = ( F ` y ) ) )
78 65 68 72 77 syl12anc 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) ( 0 <_ y /\ z = ( F ` y ) ) )
79 iftrue 
 |-  ( 0 <_ y -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = ( F ` y ) )
80 79 eqeq2d 
 |-  ( 0 <_ y -> ( z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) <-> z = ( F ` y ) ) )
81 80 biimpar 
 |-  ( ( 0 <_ y /\ z = ( F ` y ) ) -> z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
82 81 reximi 
 |-  ( E. y e. ( -u 1 [,] 1 ) ( 0 <_ y /\ z = ( F ` y ) ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
83 78 82 syl 
 |-  ( ( z e. RR* /\ 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
84 xnegcl 
 |-  ( z e. RR* -> -e z e. RR* )
85 84 adantr 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -e z e. RR* )
86 0xr 
 |-  0 e. RR*
87 xrletri 
 |-  ( ( 0 e. RR* /\ z e. RR* ) -> ( 0 <_ z \/ z <_ 0 ) )
88 86 87 mpan 
 |-  ( z e. RR* -> ( 0 <_ z \/ z <_ 0 ) )
89 88 ord 
 |-  ( z e. RR* -> ( -. 0 <_ z -> z <_ 0 ) )
90 xle0neg1 
 |-  ( z e. RR* -> ( z <_ 0 <-> 0 <_ -e z ) )
91 89 90 sylibd 
 |-  ( z e. RR* -> ( -. 0 <_ z -> 0 <_ -e z ) )
92 91 imp 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> 0 <_ -e z )
93 elxrge0 
 |-  ( -e z e. ( 0 [,] +oo ) <-> ( -e z e. RR* /\ 0 <_ -e z ) )
94 85 92 93 sylanbrc 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -e z e. ( 0 [,] +oo ) )
95 62 ffvelrni 
 |-  ( -e z e. ( 0 [,] +oo ) -> ( `' F ` -e z ) e. ( 0 [,] 1 ) )
96 94 95 syl 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. ( 0 [,] 1 ) )
97 58 96 sseldi 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. ( -u 1 [,] 1 ) )
98 iccssre 
 |-  ( ( -u 1 e. RR /\ 1 e. RR ) -> ( -u 1 [,] 1 ) C_ RR )
99 11 12 98 mp2an 
 |-  ( -u 1 [,] 1 ) C_ RR
100 99 97 sseldi 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. RR )
101 iccneg 
 |-  ( ( -u 1 e. RR /\ 1 e. RR /\ ( `' F ` -e z ) e. RR ) -> ( ( `' F ` -e z ) e. ( -u 1 [,] 1 ) <-> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) ) )
102 11 12 101 mp3an12 
 |-  ( ( `' F ` -e z ) e. RR -> ( ( `' F ` -e z ) e. ( -u 1 [,] 1 ) <-> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) ) )
103 100 102 syl 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( `' F ` -e z ) e. ( -u 1 [,] 1 ) <-> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) ) )
104 97 103 mpbid 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) )
105 negneg1e1 
 |-  -u -u 1 = 1
106 105 oveq2i 
 |-  ( -u 1 [,] -u -u 1 ) = ( -u 1 [,] 1 )
107 104 106 eleqtrdi 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -u ( `' F ` -e z ) e. ( -u 1 [,] 1 ) )
108 xle0neg2 
 |-  ( z e. RR* -> ( 0 <_ z <-> -e z <_ 0 ) )
109 108 notbid 
 |-  ( z e. RR* -> ( -. 0 <_ z <-> -. -e z <_ 0 ) )
110 109 biimpa 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -. -e z <_ 0 )
111 f1ocnvfv2 
 |-  ( ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ -e z e. ( 0 [,] +oo ) ) -> ( F ` ( `' F ` -e z ) ) = -e z )
112 22 94 111 sylancr 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` ( `' F ` -e z ) ) = -e z )
113 0elunit 
 |-  0 e. ( 0 [,] 1 )
114 ax-1ne0 
 |-  1 =/= 0
115 neeq2 
 |-  ( x = 0 -> ( 1 =/= x <-> 1 =/= 0 ) )
116 114 115 mpbiri 
 |-  ( x = 0 -> 1 =/= x )
117 116 necomd 
 |-  ( x = 0 -> x =/= 1 )
118 ifnefalse 
 |-  ( x =/= 1 -> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) = ( x / ( 1 - x ) ) )
119 117 118 syl 
 |-  ( x = 0 -> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) = ( x / ( 1 - x ) ) )
120 id 
 |-  ( x = 0 -> x = 0 )
121 oveq2 
 |-  ( x = 0 -> ( 1 - x ) = ( 1 - 0 ) )
122 1m0e1 
 |-  ( 1 - 0 ) = 1
123 121 122 eqtrdi 
 |-  ( x = 0 -> ( 1 - x ) = 1 )
124 120 123 oveq12d 
 |-  ( x = 0 -> ( x / ( 1 - x ) ) = ( 0 / 1 ) )
125 ax-1cn 
 |-  1 e. CC
126 125 114 div0i 
 |-  ( 0 / 1 ) = 0
127 124 126 eqtrdi 
 |-  ( x = 0 -> ( x / ( 1 - x ) ) = 0 )
128 119 127 eqtrd 
 |-  ( x = 0 -> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) = 0 )
129 c0ex 
 |-  0 e. _V
130 128 1 129 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( F ` 0 ) = 0 )
131 113 130 ax-mp 
 |-  ( F ` 0 ) = 0
132 131 a1i 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` 0 ) = 0 )
133 112 132 breq12d 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) <-> -e z <_ 0 ) )
134 110 133 mtbird 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -. ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) )
135 eqid 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
136 1 135 iccpnfhmeo 
 |-  ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ F e. ( II Homeo ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) )
137 136 simpli 
 |-  F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )
138 iccssxr 
 |-  ( 0 [,] 1 ) C_ RR*
139 138 10 pm3.2i 
 |-  ( ( 0 [,] 1 ) C_ RR* /\ ( 0 [,] +oo ) C_ RR* )
140 leisorel 
 |-  ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( ( 0 [,] 1 ) C_ RR* /\ ( 0 [,] +oo ) C_ RR* ) /\ ( ( `' F ` -e z ) e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) ) -> ( ( `' F ` -e z ) <_ 0 <-> ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) ) )
141 137 139 140 mp3an12 
 |-  ( ( ( `' F ` -e z ) e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) -> ( ( `' F ` -e z ) <_ 0 <-> ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) ) )
142 96 113 141 sylancl 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( `' F ` -e z ) <_ 0 <-> ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) ) )
143 134 142 mtbird 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -. ( `' F ` -e z ) <_ 0 )
144 100 le0neg1d 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( `' F ` -e z ) <_ 0 <-> 0 <_ -u ( `' F ` -e z ) ) )
145 143 144 mtbid 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -. 0 <_ -u ( `' F ` -e z ) )
146 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
147 146 96 sseldi 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. RR )
148 147 recnd 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. CC )
149 148 negnegd 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -u -u ( `' F ` -e z ) = ( `' F ` -e z ) )
150 149 fveq2d 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` -u -u ( `' F ` -e z ) ) = ( F ` ( `' F ` -e z ) ) )
151 150 112 eqtrd 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` -u -u ( `' F ` -e z ) ) = -e z )
152 xnegeq 
 |-  ( ( F ` -u -u ( `' F ` -e z ) ) = -e z -> -e ( F ` -u -u ( `' F ` -e z ) ) = -e -e z )
153 151 152 syl 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -e ( F ` -u -u ( `' F ` -e z ) ) = -e -e z )
154 xnegneg 
 |-  ( z e. RR* -> -e -e z = z )
155 154 adantr 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> -e -e z = z )
156 153 155 eqtr2d 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> z = -e ( F ` -u -u ( `' F ` -e z ) ) )
157 breq2 
 |-  ( y = -u ( `' F ` -e z ) -> ( 0 <_ y <-> 0 <_ -u ( `' F ` -e z ) ) )
158 157 notbid 
 |-  ( y = -u ( `' F ` -e z ) -> ( -. 0 <_ y <-> -. 0 <_ -u ( `' F ` -e z ) ) )
159 negeq 
 |-  ( y = -u ( `' F ` -e z ) -> -u y = -u -u ( `' F ` -e z ) )
160 159 fveq2d 
 |-  ( y = -u ( `' F ` -e z ) -> ( F ` -u y ) = ( F ` -u -u ( `' F ` -e z ) ) )
161 xnegeq 
 |-  ( ( F ` -u y ) = ( F ` -u -u ( `' F ` -e z ) ) -> -e ( F ` -u y ) = -e ( F ` -u -u ( `' F ` -e z ) ) )
162 160 161 syl 
 |-  ( y = -u ( `' F ` -e z ) -> -e ( F ` -u y ) = -e ( F ` -u -u ( `' F ` -e z ) ) )
163 162 eqeq2d 
 |-  ( y = -u ( `' F ` -e z ) -> ( z = -e ( F ` -u y ) <-> z = -e ( F ` -u -u ( `' F ` -e z ) ) ) )
164 158 163 anbi12d 
 |-  ( y = -u ( `' F ` -e z ) -> ( ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) <-> ( -. 0 <_ -u ( `' F ` -e z ) /\ z = -e ( F ` -u -u ( `' F ` -e z ) ) ) ) )
165 164 rspcev 
 |-  ( ( -u ( `' F ` -e z ) e. ( -u 1 [,] 1 ) /\ ( -. 0 <_ -u ( `' F ` -e z ) /\ z = -e ( F ` -u -u ( `' F ` -e z ) ) ) ) -> E. y e. ( -u 1 [,] 1 ) ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) )
166 107 145 156 165 syl12anc 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) )
167 iffalse 
 |-  ( -. 0 <_ y -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = -e ( F ` -u y ) )
168 167 eqeq2d 
 |-  ( -. 0 <_ y -> ( z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) <-> z = -e ( F ` -u y ) ) )
169 168 biimpar 
 |-  ( ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) -> z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
170 169 reximi 
 |-  ( E. y e. ( -u 1 [,] 1 ) ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
171 166 170 syl 
 |-  ( ( z e. RR* /\ -. 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
172 83 171 pm2.61dan 
 |-  ( z e. RR* -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
173 51 172 mprgbir 
 |-  RR* C_ { z | E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) }
174 2 rnmpt 
 |-  ran G = { z | E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) }
175 173 174 sseqtrri 
 |-  RR* C_ ran G
176 50 175 eqssi 
 |-  ran G = RR*
177 dffo2 
 |-  ( G : ( -u 1 [,] 1 ) -onto-> RR* <-> ( G : ( -u 1 [,] 1 ) --> RR* /\ ran G = RR* ) )
178 48 176 177 mpbir2an 
 |-  G : ( -u 1 [,] 1 ) -onto-> RR*
179 breq1 
 |-  ( ( F ` z ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) -> ( ( F ` z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) <-> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
180 breq1 
 |-  ( -e ( F ` -u z ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) -> ( -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) <-> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
181 simpl3 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z < w )
182 simpl1 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z e. ( -u 1 [,] 1 ) )
183 simpr 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> 0 <_ z )
184 breq2 
 |-  ( y = z -> ( 0 <_ y <-> 0 <_ z ) )
185 eleq1w 
 |-  ( y = z -> ( y e. ( 0 [,] 1 ) <-> z e. ( 0 [,] 1 ) ) )
186 184 185 imbi12d 
 |-  ( y = z -> ( ( 0 <_ y -> y e. ( 0 [,] 1 ) ) <-> ( 0 <_ z -> z e. ( 0 [,] 1 ) ) ) )
187 20 ex 
 |-  ( y e. ( -u 1 [,] 1 ) -> ( 0 <_ y -> y e. ( 0 [,] 1 ) ) )
188 186 187 vtoclga 
 |-  ( z e. ( -u 1 [,] 1 ) -> ( 0 <_ z -> z e. ( 0 [,] 1 ) ) )
189 182 183 188 sylc 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z e. ( 0 [,] 1 ) )
190 simpl2 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> w e. ( -u 1 [,] 1 ) )
191 30 a1i 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> 0 e. RR )
192 99 182 sseldi 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z e. RR )
193 99 190 sseldi 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> w e. RR )
194 192 193 181 ltled 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z <_ w )
195 191 192 193 183 194 letrd 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> 0 <_ w )
196 breq2 
 |-  ( y = w -> ( 0 <_ y <-> 0 <_ w ) )
197 eleq1w 
 |-  ( y = w -> ( y e. ( 0 [,] 1 ) <-> w e. ( 0 [,] 1 ) ) )
198 196 197 imbi12d 
 |-  ( y = w -> ( ( 0 <_ y -> y e. ( 0 [,] 1 ) ) <-> ( 0 <_ w -> w e. ( 0 [,] 1 ) ) ) )
199 198 187 vtoclga 
 |-  ( w e. ( -u 1 [,] 1 ) -> ( 0 <_ w -> w e. ( 0 [,] 1 ) ) )
200 190 195 199 sylc 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> w e. ( 0 [,] 1 ) )
201 isorel 
 |-  ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( z e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) ) -> ( z < w <-> ( F ` z ) < ( F ` w ) ) )
202 137 201 mpan 
 |-  ( ( z e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) -> ( z < w <-> ( F ` z ) < ( F ` w ) ) )
203 189 200 202 syl2anc 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> ( z < w <-> ( F ` z ) < ( F ` w ) ) )
204 181 203 mpbid 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> ( F ` z ) < ( F ` w ) )
205 195 iftrued 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) = ( F ` w ) )
206 204 205 breqtrrd 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> ( F ` z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
207 breq2 
 |-  ( ( F ` w ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) -> ( -e ( F ` -u z ) < ( F ` w ) <-> -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
208 breq2 
 |-  ( -e ( F ` -u w ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) -> ( -e ( F ` -u z ) < -e ( F ` -u w ) <-> -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
209 simpl1 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> z e. ( -u 1 [,] 1 ) )
210 simpr 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> -. 0 <_ z )
211 184 notbid 
 |-  ( y = z -> ( -. 0 <_ y <-> -. 0 <_ z ) )
212 negeq 
 |-  ( y = z -> -u y = -u z )
213 212 eleq1d 
 |-  ( y = z -> ( -u y e. ( 0 [,] 1 ) <-> -u z e. ( 0 [,] 1 ) ) )
214 211 213 imbi12d 
 |-  ( y = z -> ( ( -. 0 <_ y -> -u y e. ( 0 [,] 1 ) ) <-> ( -. 0 <_ z -> -u z e. ( 0 [,] 1 ) ) ) )
215 42 ex 
 |-  ( y e. ( -u 1 [,] 1 ) -> ( -. 0 <_ y -> -u y e. ( 0 [,] 1 ) ) )
216 214 215 vtoclga 
 |-  ( z e. ( -u 1 [,] 1 ) -> ( -. 0 <_ z -> -u z e. ( 0 [,] 1 ) ) )
217 209 210 216 sylc 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> -u z e. ( 0 [,] 1 ) )
218 217 adantr 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -u z e. ( 0 [,] 1 ) )
219 24 ffvelrni 
 |-  ( -u z e. ( 0 [,] 1 ) -> ( F ` -u z ) e. ( 0 [,] +oo ) )
220 218 219 syl 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` -u z ) e. ( 0 [,] +oo ) )
221 10 220 sseldi 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` -u z ) e. RR* )
222 221 xnegcld 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -e ( F ` -u z ) e. RR* )
223 86 a1i 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 e. RR* )
224 simpll2 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> w e. ( -u 1 [,] 1 ) )
225 simpr 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 <_ w )
226 224 225 199 sylc 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> w e. ( 0 [,] 1 ) )
227 24 ffvelrni 
 |-  ( w e. ( 0 [,] 1 ) -> ( F ` w ) e. ( 0 [,] +oo ) )
228 226 227 syl 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` w ) e. ( 0 [,] +oo ) )
229 10 228 sseldi 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` w ) e. RR* )
230 210 adantr 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -. 0 <_ z )
231 simpll1 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> z e. ( -u 1 [,] 1 ) )
232 99 231 sseldi 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> z e. RR )
233 ltnle 
 |-  ( ( z e. RR /\ 0 e. RR ) -> ( z < 0 <-> -. 0 <_ z ) )
234 232 30 233 sylancl 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( z < 0 <-> -. 0 <_ z ) )
235 230 234 mpbird 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> z < 0 )
236 232 lt0neg1d 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( z < 0 <-> 0 < -u z ) )
237 235 236 mpbid 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 < -u z )
238 isorel 
 |-  ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( 0 e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) ) -> ( 0 < -u z <-> ( F ` 0 ) < ( F ` -u z ) ) )
239 137 238 mpan 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) -> ( 0 < -u z <-> ( F ` 0 ) < ( F ` -u z ) ) )
240 113 218 239 sylancr 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( 0 < -u z <-> ( F ` 0 ) < ( F ` -u z ) ) )
241 237 240 mpbid 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` 0 ) < ( F ` -u z ) )
242 131 241 eqbrtrrid 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 < ( F ` -u z ) )
243 xlt0neg2 
 |-  ( ( F ` -u z ) e. RR* -> ( 0 < ( F ` -u z ) <-> -e ( F ` -u z ) < 0 ) )
244 221 243 syl 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( 0 < ( F ` -u z ) <-> -e ( F ` -u z ) < 0 ) )
245 242 244 mpbid 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -e ( F ` -u z ) < 0 )
246 elxrge0 
 |-  ( ( F ` w ) e. ( 0 [,] +oo ) <-> ( ( F ` w ) e. RR* /\ 0 <_ ( F ` w ) ) )
247 246 simprbi 
 |-  ( ( F ` w ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` w ) )
248 228 247 syl 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 <_ ( F ` w ) )
249 222 223 229 245 248 xrltletrd 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -e ( F ` -u z ) < ( F ` w ) )
250 simpll3 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> z < w )
251 simpll1 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> z e. ( -u 1 [,] 1 ) )
252 99 251 sseldi 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> z e. RR )
253 simpll2 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> w e. ( -u 1 [,] 1 ) )
254 99 253 sseldi 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> w e. RR )
255 252 254 ltnegd 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( z < w <-> -u w < -u z ) )
256 250 255 mpbid 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -u w < -u z )
257 simpr 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -. 0 <_ w )
258 196 notbid 
 |-  ( y = w -> ( -. 0 <_ y <-> -. 0 <_ w ) )
259 negeq 
 |-  ( y = w -> -u y = -u w )
260 259 eleq1d 
 |-  ( y = w -> ( -u y e. ( 0 [,] 1 ) <-> -u w e. ( 0 [,] 1 ) ) )
261 258 260 imbi12d 
 |-  ( y = w -> ( ( -. 0 <_ y -> -u y e. ( 0 [,] 1 ) ) <-> ( -. 0 <_ w -> -u w e. ( 0 [,] 1 ) ) ) )
262 261 215 vtoclga 
 |-  ( w e. ( -u 1 [,] 1 ) -> ( -. 0 <_ w -> -u w e. ( 0 [,] 1 ) ) )
263 253 257 262 sylc 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -u w e. ( 0 [,] 1 ) )
264 217 adantr 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -u z e. ( 0 [,] 1 ) )
265 isorel 
 |-  ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( -u w e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) ) -> ( -u w < -u z <-> ( F ` -u w ) < ( F ` -u z ) ) )
266 137 265 mpan 
 |-  ( ( -u w e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) -> ( -u w < -u z <-> ( F ` -u w ) < ( F ` -u z ) ) )
267 263 264 266 syl2anc 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( -u w < -u z <-> ( F ` -u w ) < ( F ` -u z ) ) )
268 256 267 mpbid 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u w ) < ( F ` -u z ) )
269 24 ffvelrni 
 |-  ( -u w e. ( 0 [,] 1 ) -> ( F ` -u w ) e. ( 0 [,] +oo ) )
270 263 269 syl 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u w ) e. ( 0 [,] +oo ) )
271 10 270 sseldi 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u w ) e. RR* )
272 264 219 syl 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u z ) e. ( 0 [,] +oo ) )
273 10 272 sseldi 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u z ) e. RR* )
274 xltneg 
 |-  ( ( ( F ` -u w ) e. RR* /\ ( F ` -u z ) e. RR* ) -> ( ( F ` -u w ) < ( F ` -u z ) <-> -e ( F ` -u z ) < -e ( F ` -u w ) ) )
275 271 273 274 syl2anc 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( ( F ` -u w ) < ( F ` -u z ) <-> -e ( F ` -u z ) < -e ( F ` -u w ) ) )
276 268 275 mpbid 
 |-  ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -e ( F ` -u z ) < -e ( F ` -u w ) )
277 207 208 249 276 ifbothda 
 |-  ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
278 179 180 206 277 ifbothda 
 |-  ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) -> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
279 278 3expia 
 |-  ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) ) -> ( z < w -> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
280 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
281 212 fveq2d 
 |-  ( y = z -> ( F ` -u y ) = ( F ` -u z ) )
282 xnegeq 
 |-  ( ( F ` -u y ) = ( F ` -u z ) -> -e ( F ` -u y ) = -e ( F ` -u z ) )
283 281 282 syl 
 |-  ( y = z -> -e ( F ` -u y ) = -e ( F ` -u z ) )
284 184 280 283 ifbieq12d 
 |-  ( y = z -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) )
285 fvex 
 |-  ( F ` z ) e. _V
286 xnegex 
 |-  -e ( F ` -u z ) e. _V
287 285 286 ifex 
 |-  if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) e. _V
288 284 2 287 fvmpt 
 |-  ( z e. ( -u 1 [,] 1 ) -> ( G ` z ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) )
289 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
290 259 fveq2d 
 |-  ( y = w -> ( F ` -u y ) = ( F ` -u w ) )
291 xnegeq 
 |-  ( ( F ` -u y ) = ( F ` -u w ) -> -e ( F ` -u y ) = -e ( F ` -u w ) )
292 290 291 syl 
 |-  ( y = w -> -e ( F ` -u y ) = -e ( F ` -u w ) )
293 196 289 292 ifbieq12d 
 |-  ( y = w -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
294 fvex 
 |-  ( F ` w ) e. _V
295 xnegex 
 |-  -e ( F ` -u w ) e. _V
296 294 295 ifex 
 |-  if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) e. _V
297 293 2 296 fvmpt 
 |-  ( w e. ( -u 1 [,] 1 ) -> ( G ` w ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
298 288 297 breqan12d 
 |-  ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) ) -> ( ( G ` z ) < ( G ` w ) <-> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
299 279 298 sylibrd 
 |-  ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) ) -> ( z < w -> ( G ` z ) < ( G ` w ) ) )
300 299 rgen2 
 |-  A. z e. ( -u 1 [,] 1 ) A. w e. ( -u 1 [,] 1 ) ( z < w -> ( G ` z ) < ( G ` w ) )
301 soisoi 
 |-  ( ( ( < Or ( -u 1 [,] 1 ) /\ < Po RR* ) /\ ( G : ( -u 1 [,] 1 ) -onto-> RR* /\ A. z e. ( -u 1 [,] 1 ) A. w e. ( -u 1 [,] 1 ) ( z < w -> ( G ` z ) < ( G ` w ) ) ) ) -> G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) )
302 7 9 178 300 301 mp4an 
 |-  G Isom < , < ( ( -u 1 [,] 1 ) , RR* )
303 letsr 
 |-  <_ e. TosetRel
304 303 elexi 
 |-  <_ e. _V
305 304 inex1 
 |-  ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) e. _V
306 ssid 
 |-  RR* C_ RR*
307 leiso 
 |-  ( ( ( -u 1 [,] 1 ) C_ RR* /\ RR* C_ RR* ) -> ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) <-> G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* ) ) )
308 4 306 307 mp2an 
 |-  ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) <-> G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* ) )
309 302 308 mpbi 
 |-  G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* )
310 isores1 
 |-  ( G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* ) <-> G Isom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) , <_ ( ( -u 1 [,] 1 ) , RR* ) )
311 309 310 mpbi 
 |-  G Isom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) , <_ ( ( -u 1 [,] 1 ) , RR* )
312 tsrps 
 |-  ( <_ e. TosetRel -> <_ e. PosetRel )
313 303 312 ax-mp 
 |-  <_ e. PosetRel
314 ledm 
 |-  RR* = dom <_
315 314 psssdm 
 |-  ( ( <_ e. PosetRel /\ ( -u 1 [,] 1 ) C_ RR* ) -> dom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) = ( -u 1 [,] 1 ) )
316 313 4 315 mp2an 
 |-  dom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) = ( -u 1 [,] 1 )
317 316 eqcomi 
 |-  ( -u 1 [,] 1 ) = dom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) )
318 317 314 ordthmeo 
 |-  ( ( ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) e. _V /\ <_ e. TosetRel /\ G Isom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) , <_ ( ( -u 1 [,] 1 ) , RR* ) ) -> G e. ( ( ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) ) Homeo ( ordTop ` <_ ) ) )
319 305 303 311 318 mp3an 
 |-  G e. ( ( ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) ) Homeo ( ordTop ` <_ ) )
320 eqid 
 |-  ( ordTop ` <_ ) = ( ordTop ` <_ )
321 3 320 xrrest2 
 |-  ( ( -u 1 [,] 1 ) C_ RR -> ( J |`t ( -u 1 [,] 1 ) ) = ( ( ordTop ` <_ ) |`t ( -u 1 [,] 1 ) ) )
322 99 321 ax-mp 
 |-  ( J |`t ( -u 1 [,] 1 ) ) = ( ( ordTop ` <_ ) |`t ( -u 1 [,] 1 ) )
323 ordtresticc 
 |-  ( ( ordTop ` <_ ) |`t ( -u 1 [,] 1 ) ) = ( ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) )
324 322 323 eqtri 
 |-  ( J |`t ( -u 1 [,] 1 ) ) = ( ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) )
325 324 oveq1i 
 |-  ( ( J |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) = ( ( ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) ) Homeo ( ordTop ` <_ ) )
326 319 325 eleqtrri 
 |-  G e. ( ( J |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) )
327 302 326 pm3.2i 
 |-  ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) /\ G e. ( ( J |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) )