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=x01ifx=1+∞x1x
xrhmeo.g G=y11if0yFyFy
xrhmeo.j J=TopOpenfld
Assertion xrhmeo GIsom<,<11*GJ𝑡11HomeoordTop

Proof

Step Hyp Ref Expression
1 xrhmeo.f F=x01ifx=1+∞x1x
2 xrhmeo.g G=y11if0yFyFy
3 xrhmeo.j J=TopOpenfld
4 iccssxr 11*
5 xrltso <Or*
6 soss 11*<Or*<Or11
7 4 5 6 mp2 <Or11
8 sopo <Or*<Po*
9 5 8 ax-mp <Po*
10 iccssxr 0+∞*
11 neg1rr 1
12 1re 1
13 11 12 elicc2i y11y1yy1
14 13 simp1bi y11y
15 14 adantr y110yy
16 simpr y110y0y
17 13 simp3bi y11y1
18 17 adantr y110yy1
19 elicc01 y01y0yy1
20 15 16 18 19 syl3anbrc y110yy01
21 1 iccpnfcnv F:011-1 onto0+∞F-1=v0+∞ifv=+∞1v1+v
22 21 simpli F:011-1 onto0+∞
23 f1of F:011-1 onto0+∞F:010+∞
24 22 23 ax-mp F:010+∞
25 24 ffvelrni y01Fy0+∞
26 20 25 syl y110yFy0+∞
27 10 26 sselid y110yFy*
28 14 adantr y11¬0yy
29 28 renegcld y11¬0yy
30 0re 0
31 letric 0y0yy0
32 30 14 31 sylancr y110yy0
33 32 orcanai y11¬0yy0
34 28 le0neg1d y11¬0yy00y
35 33 34 mpbid y11¬0y0y
36 13 simp2bi y111y
37 36 adantr y11¬0y1y
38 lenegcon1 1y1yy1
39 12 28 38 sylancr y11¬0y1yy1
40 37 39 mpbid y11¬0yy1
41 elicc01 y01y0yy1
42 29 35 40 41 syl3anbrc y11¬0yy01
43 24 ffvelrni y01Fy0+∞
44 42 43 syl y11¬0yFy0+∞
45 10 44 sselid y11¬0yFy*
46 45 xnegcld y11¬0yFy*
47 27 46 ifclda y11if0yFyFy*
48 2 47 fmpti G:11*
49 frn G:11*ranG*
50 48 49 ax-mp ranG*
51 ssabral *z|y11z=if0yFyFyz*y11z=if0yFyFy
52 0le1 01
53 le0neg2 10110
54 12 53 ax-mp 0110
55 52 54 mpbi 10
56 1le1 11
57 iccss 1110110111
58 11 12 55 56 57 mp4an 0111
59 elxrge0 z0+∞z*0z
60 f1ocnv F:011-1 onto0+∞F-1:0+∞1-1 onto01
61 f1of F-1:0+∞1-1 onto01F-1:0+∞01
62 22 60 61 mp2b F-1:0+∞01
63 62 ffvelrni z0+∞F-1z01
64 59 63 sylbir z*0zF-1z01
65 58 64 sselid z*0zF-1z11
66 elicc01 F-1z01F-1z0F-1zF-1z1
67 66 simp2bi F-1z010F-1z
68 64 67 syl z*0z0F-1z
69 59 biimpri z*0zz0+∞
70 f1ocnvfv2 F:011-1 onto0+∞z0+∞FF-1z=z
71 22 69 70 sylancr z*0zFF-1z=z
72 71 eqcomd z*0zz=FF-1z
73 breq2 y=F-1z0y0F-1z
74 fveq2 y=F-1zFy=FF-1z
75 74 eqeq2d y=F-1zz=Fyz=FF-1z
76 73 75 anbi12d y=F-1z0yz=Fy0F-1zz=FF-1z
77 76 rspcev F-1z110F-1zz=FF-1zy110yz=Fy
78 65 68 72 77 syl12anc z*0zy110yz=Fy
79 iftrue 0yif0yFyFy=Fy
80 79 eqeq2d 0yz=if0yFyFyz=Fy
81 80 biimpar 0yz=Fyz=if0yFyFy
82 81 reximi y110yz=Fyy11z=if0yFyFy
83 78 82 syl z*0zy11z=if0yFyFy
84 xnegcl z*z*
85 84 adantr z*¬0zz*
86 0xr 0*
87 xrletri 0*z*0zz0
88 86 87 mpan z*0zz0
89 88 ord z*¬0zz0
90 xle0neg1 z*z00z
91 89 90 sylibd z*¬0z0z
92 91 imp z*¬0z0z
93 elxrge0 z0+∞z*0z
94 85 92 93 sylanbrc z*¬0zz0+∞
95 62 ffvelrni z0+∞F-1z01
96 94 95 syl z*¬0zF-1z01
97 58 96 sselid z*¬0zF-1z11
98 iccssre 1111
99 11 12 98 mp2an 11
100 99 97 sselid z*¬0zF-1z
101 iccneg 11F-1zF-1z11F-1z1-1
102 11 12 101 mp3an12 F-1zF-1z11F-1z1-1
103 100 102 syl z*¬0zF-1z11F-1z1-1
104 97 103 mpbid z*¬0zF-1z1-1
105 negneg1e1 -1=1
106 105 oveq2i 1-1=11
107 104 106 eleqtrdi z*¬0zF-1z11
108 xle0neg2 z*0zz0
109 108 notbid z*¬0z¬z0
110 109 biimpa z*¬0z¬z0
111 f1ocnvfv2 F:011-1 onto0+∞z0+∞FF-1z=z
112 22 94 111 sylancr z*¬0zFF-1z=z
113 0elunit 001
114 ax-1ne0 10
115 neeq2 x=01x10
116 114 115 mpbiri x=01x
117 116 necomd x=0x1
118 ifnefalse x1ifx=1+∞x1x=x1x
119 117 118 syl x=0ifx=1+∞x1x=x1x
120 id x=0x=0
121 oveq2 x=01x=10
122 1m0e1 10=1
123 121 122 eqtrdi x=01x=1
124 120 123 oveq12d x=0x1x=01
125 ax-1cn 1
126 125 114 div0i 01=0
127 124 126 eqtrdi x=0x1x=0
128 119 127 eqtrd x=0ifx=1+∞x1x=0
129 c0ex 0V
130 128 1 129 fvmpt 001F0=0
131 113 130 ax-mp F0=0
132 131 a1i z*¬0zF0=0
133 112 132 breq12d z*¬0zFF-1zF0z0
134 110 133 mtbird z*¬0z¬FF-1zF0
135 eqid ordTop𝑡0+∞=ordTop𝑡0+∞
136 1 135 iccpnfhmeo FIsom<,<010+∞FIIHomeoordTop𝑡0+∞
137 136 simpli FIsom<,<010+∞
138 iccssxr 01*
139 138 10 pm3.2i 01*0+∞*
140 leisorel FIsom<,<010+∞01*0+∞*F-1z01001F-1z0FF-1zF0
141 137 139 140 mp3an12 F-1z01001F-1z0FF-1zF0
142 96 113 141 sylancl z*¬0zF-1z0FF-1zF0
143 134 142 mtbird z*¬0z¬F-1z0
144 100 le0neg1d z*¬0zF-1z00F-1z
145 143 144 mtbid z*¬0z¬0F-1z
146 unitssre 01
147 146 96 sselid z*¬0zF-1z
148 147 recnd z*¬0zF-1z
149 148 negnegd z*¬0zF-1z=F-1z
150 149 fveq2d z*¬0zFF-1z=FF-1z
151 150 112 eqtrd z*¬0zFF-1z=z
152 xnegeq FF-1z=zFF-1z=z
153 151 152 syl z*¬0zFF-1z=z
154 xnegneg z*z=z
155 154 adantr z*¬0zz=z
156 153 155 eqtr2d z*¬0zz=FF-1z
157 breq2 y=F-1z0y0F-1z
158 157 notbid y=F-1z¬0y¬0F-1z
159 negeq y=F-1zy=F-1z
160 159 fveq2d y=F-1zFy=FF-1z
161 xnegeq Fy=FF-1zFy=FF-1z
162 160 161 syl y=F-1zFy=FF-1z
163 162 eqeq2d y=F-1zz=Fyz=FF-1z
164 158 163 anbi12d y=F-1z¬0yz=Fy¬0F-1zz=FF-1z
165 164 rspcev F-1z11¬0F-1zz=FF-1zy11¬0yz=Fy
166 107 145 156 165 syl12anc z*¬0zy11¬0yz=Fy
167 iffalse ¬0yif0yFyFy=Fy
168 167 eqeq2d ¬0yz=if0yFyFyz=Fy
169 168 biimpar ¬0yz=Fyz=if0yFyFy
170 169 reximi y11¬0yz=Fyy11z=if0yFyFy
171 166 170 syl z*¬0zy11z=if0yFyFy
172 83 171 pm2.61dan z*y11z=if0yFyFy
173 51 172 mprgbir *z|y11z=if0yFyFy
174 2 rnmpt ranG=z|y11z=if0yFyFy
175 173 174 sseqtrri *ranG
176 50 175 eqssi ranG=*
177 dffo2 G:11onto*G:11*ranG=*
178 48 176 177 mpbir2an G:11onto*
179 breq1 Fz=if0zFzFzFz<if0wFwFwif0zFzFz<if0wFwFw
180 breq1 Fz=if0zFzFzFz<if0wFwFwif0zFzFz<if0wFwFw
181 simpl3 z11w11z<w0zz<w
182 simpl1 z11w11z<w0zz11
183 simpr z11w11z<w0z0z
184 breq2 y=z0y0z
185 eleq1w y=zy01z01
186 184 185 imbi12d y=z0yy010zz01
187 20 ex y110yy01
188 186 187 vtoclga z110zz01
189 182 183 188 sylc z11w11z<w0zz01
190 simpl2 z11w11z<w0zw11
191 30 a1i z11w11z<w0z0
192 99 182 sselid z11w11z<w0zz
193 99 190 sselid z11w11z<w0zw
194 192 193 181 ltled z11w11z<w0zzw
195 191 192 193 183 194 letrd z11w11z<w0z0w
196 breq2 y=w0y0w
197 eleq1w y=wy01w01
198 196 197 imbi12d y=w0yy010ww01
199 198 187 vtoclga w110ww01
200 190 195 199 sylc z11w11z<w0zw01
201 isorel FIsom<,<010+∞z01w01z<wFz<Fw
202 137 201 mpan z01w01z<wFz<Fw
203 189 200 202 syl2anc z11w11z<w0zz<wFz<Fw
204 181 203 mpbid z11w11z<w0zFz<Fw
205 195 iftrued z11w11z<w0zif0wFwFw=Fw
206 204 205 breqtrrd z11w11z<w0zFz<if0wFwFw
207 breq2 Fw=if0wFwFwFz<FwFz<if0wFwFw
208 breq2 Fw=if0wFwFwFz<FwFz<if0wFwFw
209 simpl1 z11w11z<w¬0zz11
210 simpr z11w11z<w¬0z¬0z
211 184 notbid y=z¬0y¬0z
212 negeq y=zy=z
213 212 eleq1d y=zy01z01
214 211 213 imbi12d y=z¬0yy01¬0zz01
215 42 ex y11¬0yy01
216 214 215 vtoclga z11¬0zz01
217 209 210 216 sylc z11w11z<w¬0zz01
218 217 adantr z11w11z<w¬0z0wz01
219 24 ffvelrni z01Fz0+∞
220 218 219 syl z11w11z<w¬0z0wFz0+∞
221 10 220 sselid z11w11z<w¬0z0wFz*
222 221 xnegcld z11w11z<w¬0z0wFz*
223 86 a1i z11w11z<w¬0z0w0*
224 simpll2 z11w11z<w¬0z0ww11
225 simpr z11w11z<w¬0z0w0w
226 224 225 199 sylc z11w11z<w¬0z0ww01
227 24 ffvelrni w01Fw0+∞
228 226 227 syl z11w11z<w¬0z0wFw0+∞
229 10 228 sselid z11w11z<w¬0z0wFw*
230 210 adantr z11w11z<w¬0z0w¬0z
231 simpll1 z11w11z<w¬0z0wz11
232 99 231 sselid z11w11z<w¬0z0wz
233 ltnle z0z<0¬0z
234 232 30 233 sylancl z11w11z<w¬0z0wz<0¬0z
235 230 234 mpbird z11w11z<w¬0z0wz<0
236 232 lt0neg1d z11w11z<w¬0z0wz<00<z
237 235 236 mpbid z11w11z<w¬0z0w0<z
238 isorel FIsom<,<010+∞001z010<zF0<Fz
239 137 238 mpan 001z010<zF0<Fz
240 113 218 239 sylancr z11w11z<w¬0z0w0<zF0<Fz
241 237 240 mpbid z11w11z<w¬0z0wF0<Fz
242 131 241 eqbrtrrid z11w11z<w¬0z0w0<Fz
243 xlt0neg2 Fz*0<FzFz<0
244 221 243 syl z11w11z<w¬0z0w0<FzFz<0
245 242 244 mpbid z11w11z<w¬0z0wFz<0
246 elxrge0 Fw0+∞Fw*0Fw
247 246 simprbi Fw0+∞0Fw
248 228 247 syl z11w11z<w¬0z0w0Fw
249 222 223 229 245 248 xrltletrd z11w11z<w¬0z0wFz<Fw
250 simpll3 z11w11z<w¬0z¬0wz<w
251 simpll1 z11w11z<w¬0z¬0wz11
252 99 251 sselid z11w11z<w¬0z¬0wz
253 simpll2 z11w11z<w¬0z¬0ww11
254 99 253 sselid z11w11z<w¬0z¬0ww
255 252 254 ltnegd z11w11z<w¬0z¬0wz<ww<z
256 250 255 mpbid z11w11z<w¬0z¬0ww<z
257 simpr z11w11z<w¬0z¬0w¬0w
258 196 notbid y=w¬0y¬0w
259 negeq y=wy=w
260 259 eleq1d y=wy01w01
261 258 260 imbi12d y=w¬0yy01¬0ww01
262 261 215 vtoclga w11¬0ww01
263 253 257 262 sylc z11w11z<w¬0z¬0ww01
264 217 adantr z11w11z<w¬0z¬0wz01
265 isorel FIsom<,<010+∞w01z01w<zFw<Fz
266 137 265 mpan w01z01w<zFw<Fz
267 263 264 266 syl2anc z11w11z<w¬0z¬0ww<zFw<Fz
268 256 267 mpbid z11w11z<w¬0z¬0wFw<Fz
269 24 ffvelrni w01Fw0+∞
270 263 269 syl z11w11z<w¬0z¬0wFw0+∞
271 10 270 sselid z11w11z<w¬0z¬0wFw*
272 264 219 syl z11w11z<w¬0z¬0wFz0+∞
273 10 272 sselid z11w11z<w¬0z¬0wFz*
274 xltneg Fw*Fz*Fw<FzFz<Fw
275 271 273 274 syl2anc z11w11z<w¬0z¬0wFw<FzFz<Fw
276 268 275 mpbid z11w11z<w¬0z¬0wFz<Fw
277 207 208 249 276 ifbothda z11w11z<w¬0zFz<if0wFwFw
278 179 180 206 277 ifbothda z11w11z<wif0zFzFz<if0wFwFw
279 278 3expia z11w11z<wif0zFzFz<if0wFwFw
280 fveq2 y=zFy=Fz
281 212 fveq2d y=zFy=Fz
282 xnegeq Fy=FzFy=Fz
283 281 282 syl y=zFy=Fz
284 184 280 283 ifbieq12d y=zif0yFyFy=if0zFzFz
285 fvex FzV
286 xnegex FzV
287 285 286 ifex if0zFzFzV
288 284 2 287 fvmpt z11Gz=if0zFzFz
289 fveq2 y=wFy=Fw
290 259 fveq2d y=wFy=Fw
291 xnegeq Fy=FwFy=Fw
292 290 291 syl y=wFy=Fw
293 196 289 292 ifbieq12d y=wif0yFyFy=if0wFwFw
294 fvex FwV
295 xnegex FwV
296 294 295 ifex if0wFwFwV
297 293 2 296 fvmpt w11Gw=if0wFwFw
298 288 297 breqan12d z11w11Gz<Gwif0zFzFz<if0wFwFw
299 279 298 sylibrd z11w11z<wGz<Gw
300 299 rgen2 z11w11z<wGz<Gw
301 soisoi <Or11<Po*G:11onto*z11w11z<wGz<GwGIsom<,<11*
302 7 9 178 300 301 mp4an GIsom<,<11*
303 letsr TosetRel
304 303 elexi V
305 304 inex1 11×11V
306 ssid **
307 leiso 11***GIsom<,<11*GIsom,11*
308 4 306 307 mp2an GIsom<,<11*GIsom,11*
309 302 308 mpbi GIsom,11*
310 isores1 GIsom,11*GIsom11×11,11*
311 309 310 mpbi GIsom11×11,11*
312 tsrps TosetRelPosetRel
313 303 312 ax-mp PosetRel
314 ledm *=dom
315 314 psssdm PosetRel11*dom11×11=11
316 313 4 315 mp2an dom11×11=11
317 316 eqcomi 11=dom11×11
318 317 314 ordthmeo 11×11VTosetRelGIsom11×11,11*GordTop11×11HomeoordTop
319 305 303 311 318 mp3an GordTop11×11HomeoordTop
320 eqid ordTop=ordTop
321 3 320 xrrest2 11J𝑡11=ordTop𝑡11
322 99 321 ax-mp J𝑡11=ordTop𝑡11
323 ordtresticc ordTop𝑡11=ordTop11×11
324 322 323 eqtri J𝑡11=ordTop11×11
325 324 oveq1i J𝑡11HomeoordTop=ordTop11×11HomeoordTop
326 319 325 eleqtrri GJ𝑡11HomeoordTop
327 302 326 pm3.2i GIsom<,<11*GJ𝑡11HomeoordTop