MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrhmeo Structured version   Visualization version   GIF version
Theorem xrhmeo 24454
Description: The bijection from [-1, 1] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
Hypotheses
Ref Expression
xrhmeo.f 𝐹 = (π‘₯ ∈ (0[,]1) ↦ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))))
xrhmeo.g 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
xrhmeo.j 𝐽 = (TopOpenβ€˜β„‚fld)
Assertion
Ref Expression
xrhmeo (𝐺 Isom < , < ((-1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ )))
Distinct variable groups:   π‘₯,𝑦   𝑦,𝐹   π‘₯,𝐽,𝑦
Allowed substitution hints:   𝐹(π‘₯)   𝐺(π‘₯,𝑦)
Proof of Theorem xrhmeo
Dummy variables 𝑀 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iccssxr 13404 . . . 4 (-1[,]1) βŠ† ℝ*
2 xrltso 13117 . . . 4 < Or ℝ*
3 soss 5608 . . . 4 ((-1[,]1) βŠ† ℝ* β†’ ( < Or ℝ* β†’ < Or (-1[,]1)))
41, 2, 3mp2 9 . . 3 < Or (-1[,]1)
5 sopo 5607 . . . 4 ( < Or ℝ* β†’ < Po ℝ*)
62, 5ax-mp 5 . . 3 < Po ℝ*
7 xrhmeo.g . . . . 5 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8 iccssxr 13404 . . . . . . 7 (0[,]+∞) βŠ† ℝ*
9 neg1rr 12324 . . . . . . . . . . . 12 -1 ∈ ℝ
10 1re 11211 . . . . . . . . . . . 12 1 ∈ ℝ
119, 10elicc2i 13387 . . . . . . . . . . 11 (𝑦 ∈ (-1[,]1) ↔ (𝑦 ∈ ℝ ∧ -1 ≀ 𝑦 ∧ 𝑦 ≀ 1))
1211simp1bi 1146 . . . . . . . . . 10 (𝑦 ∈ (-1[,]1) β†’ 𝑦 ∈ ℝ)
1312adantr 482 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 𝑦 ∈ ℝ)
14 simpr 486 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 0 ≀ 𝑦)
1511simp3bi 1148 . . . . . . . . . 10 (𝑦 ∈ (-1[,]1) β†’ 𝑦 ≀ 1)
1615adantr 482 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 𝑦 ≀ 1)
17 elicc01 13440 . . . . . . . . 9 (𝑦 ∈ (0[,]1) ↔ (𝑦 ∈ ℝ ∧ 0 ≀ 𝑦 ∧ 𝑦 ≀ 1))
1813, 14, 16, 17syl3anbrc 1344 . . . . . . . 8 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 𝑦 ∈ (0[,]1))
19 xrhmeo.f . . . . . . . . . . . 12 𝐹 = (π‘₯ ∈ (0[,]1) ↦ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))))
2019iccpnfcnv 24452 . . . . . . . . . . 11 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ ◑𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
2120simpli 485 . . . . . . . . . 10 𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞)
22 f1of 6831 . . . . . . . . . 10 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) β†’ 𝐹:(0[,]1)⟢(0[,]+∞))
2321, 22ax-mp 5 . . . . . . . . 9 𝐹:(0[,]1)⟢(0[,]+∞)
2423ffvelcdmi 7083 . . . . . . . 8 (𝑦 ∈ (0[,]1) β†’ (πΉβ€˜π‘¦) ∈ (0[,]+∞))
2518, 24syl 17 . . . . . . 7 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ (πΉβ€˜π‘¦) ∈ (0[,]+∞))
268, 25sselid 3980 . . . . . 6 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ (πΉβ€˜π‘¦) ∈ ℝ*)
2712adantr 482 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 𝑦 ∈ ℝ)
2827renegcld 11638 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ∈ ℝ)
29 0re 11213 . . . . . . . . . . . . 13 0 ∈ ℝ
30 letric 11311 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (0 ≀ 𝑦 ∨ 𝑦 ≀ 0))
3129, 12, 30sylancr 588 . . . . . . . . . . . 12 (𝑦 ∈ (-1[,]1) β†’ (0 ≀ 𝑦 ∨ 𝑦 ≀ 0))
3231orcanai 1002 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 𝑦 ≀ 0)
3327le0neg1d 11782 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (𝑦 ≀ 0 ↔ 0 ≀ -𝑦))
3432, 33mpbid 231 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 0 ≀ -𝑦)
3511simp2bi 1147 . . . . . . . . . . . 12 (𝑦 ∈ (-1[,]1) β†’ -1 ≀ 𝑦)
3635adantr 482 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -1 ≀ 𝑦)
37 lenegcon1 11715 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (-1 ≀ 𝑦 ↔ -𝑦 ≀ 1))
3810, 27, 37sylancr 588 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (-1 ≀ 𝑦 ↔ -𝑦 ≀ 1))
3936, 38mpbid 231 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ≀ 1)
40 elicc01 13440 . . . . . . . . . 10 (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≀ -𝑦 ∧ -𝑦 ≀ 1))
4128, 34, 39, 40syl3anbrc 1344 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ∈ (0[,]1))
4223ffvelcdmi 7083 . . . . . . . . 9 (-𝑦 ∈ (0[,]1) β†’ (πΉβ€˜-𝑦) ∈ (0[,]+∞))
4341, 42syl 17 . . . . . . . 8 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (πΉβ€˜-𝑦) ∈ (0[,]+∞))
448, 43sselid 3980 . . . . . . 7 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (πΉβ€˜-𝑦) ∈ ℝ*)
4544xnegcld 13276 . . . . . 6 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑒(πΉβ€˜-𝑦) ∈ ℝ*)
4626, 45ifclda 4563 . . . . 5 (𝑦 ∈ (-1[,]1) β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ∈ ℝ*)
477, 46fmpti 7109 . . . 4 𝐺:(-1[,]1)βŸΆβ„*
48 frn 6722 . . . . . 6 (𝐺:(-1[,]1)βŸΆβ„* β†’ ran 𝐺 βŠ† ℝ*)
4947, 48ax-mp 5 . . . . 5 ran 𝐺 βŠ† ℝ*
50 ssabral 4059 . . . . . . 7 (ℝ* βŠ† {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))} ↔ βˆ€π‘§ ∈ ℝ* βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
51 0le1 11734 . . . . . . . . . . . . 13 0 ≀ 1
52 le0neg2 11720 . . . . . . . . . . . . . 14 (1 ∈ ℝ β†’ (0 ≀ 1 ↔ -1 ≀ 0))
5310, 52ax-mp 5 . . . . . . . . . . . . 13 (0 ≀ 1 ↔ -1 ≀ 0)
5451, 53mpbi 229 . . . . . . . . . . . 12 -1 ≀ 0
55 1le1 11839 . . . . . . . . . . . 12 1 ≀ 1
56 iccss 13389 . . . . . . . . . . . 12 (((-1 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (-1 ≀ 0 ∧ 1 ≀ 1)) β†’ (0[,]1) βŠ† (-1[,]1))
579, 10, 54, 55, 56mp4an 692 . . . . . . . . . . 11 (0[,]1) βŠ† (-1[,]1)
58 elxrge0 13431 . . . . . . . . . . . 12 (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧))
59 f1ocnv 6843 . . . . . . . . . . . . . 14 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) β†’ ◑𝐹:(0[,]+∞)–1-1-ontoβ†’(0[,]1))
60 f1of 6831 . . . . . . . . . . . . . 14 (◑𝐹:(0[,]+∞)–1-1-ontoβ†’(0[,]1) β†’ ◑𝐹:(0[,]+∞)⟢(0[,]1))
6121, 59, 60mp2b 10 . . . . . . . . . . . . 13 ◑𝐹:(0[,]+∞)⟢(0[,]1)
6261ffvelcdmi 7083 . . . . . . . . . . . 12 (𝑧 ∈ (0[,]+∞) β†’ (β—‘πΉβ€˜π‘§) ∈ (0[,]1))
6358, 62sylbir 234 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜π‘§) ∈ (0[,]1))
6457, 63sselid 3980 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜π‘§) ∈ (-1[,]1))
65 elicc01 13440 . . . . . . . . . . . 12 ((β—‘πΉβ€˜π‘§) ∈ (0[,]1) ↔ ((β—‘πΉβ€˜π‘§) ∈ ℝ ∧ 0 ≀ (β—‘πΉβ€˜π‘§) ∧ (β—‘πΉβ€˜π‘§) ≀ 1))
6665simp2bi 1147 . . . . . . . . . . 11 ((β—‘πΉβ€˜π‘§) ∈ (0[,]1) β†’ 0 ≀ (β—‘πΉβ€˜π‘§))
6763, 66syl 17 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 0 ≀ (β—‘πΉβ€˜π‘§))
6858biimpri 227 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ (0[,]+∞))
69 f1ocnvfv2 7272 . . . . . . . . . . . 12 ((𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘§)) = 𝑧)
7021, 68, 69sylancr 588 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘§)) = 𝑧)
7170eqcomd 2739 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))
72 breq2 5152 . . . . . . . . . . . 12 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (0 ≀ 𝑦 ↔ 0 ≀ (β—‘πΉβ€˜π‘§)))
73 fveq2 6889 . . . . . . . . . . . . 13 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜(β—‘πΉβ€˜π‘§)))
7473eqeq2d 2744 . . . . . . . . . . . 12 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (𝑧 = (πΉβ€˜π‘¦) ↔ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§))))
7572, 74anbi12d 632 . . . . . . . . . . 11 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ ((0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) ↔ (0 ≀ (β—‘πΉβ€˜π‘§) ∧ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))))
7675rspcev 3613 . . . . . . . . . 10 (((β—‘πΉβ€˜π‘§) ∈ (-1[,]1) ∧ (0 ≀ (β—‘πΉβ€˜π‘§) ∧ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)))
7764, 67, 71, 76syl12anc 836 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)))
78 iftrue 4534 . . . . . . . . . . . 12 (0 ≀ 𝑦 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = (πΉβ€˜π‘¦))
7978eqeq2d 2744 . . . . . . . . . . 11 (0 ≀ 𝑦 β†’ (𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ↔ 𝑧 = (πΉβ€˜π‘¦)))
8079biimpar 479 . . . . . . . . . 10 ((0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) β†’ 𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8180reximi 3085 . . . . . . . . 9 (βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8277, 81syl 17 . . . . . . . 8 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
83 xnegcl 13189 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℝ* β†’ -𝑒𝑧 ∈ ℝ*)
8483adantr 482 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒𝑧 ∈ ℝ*)
85 0xr 11258 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ*
86 xrletri 13129 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) β†’ (0 ≀ 𝑧 ∨ 𝑧 ≀ 0))
8785, 86mpan 689 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℝ* β†’ (0 ≀ 𝑧 ∨ 𝑧 ≀ 0))
8887ord 863 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 β†’ 𝑧 ≀ 0))
89 xle0neg1 13197 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℝ* β†’ (𝑧 ≀ 0 ↔ 0 ≀ -𝑒𝑧))
9088, 89sylibd 238 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 β†’ 0 ≀ -𝑒𝑧))
9190imp 408 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ 0 ≀ -𝑒𝑧)
92 elxrge0 13431 . . . . . . . . . . . . . . 15 (-𝑒𝑧 ∈ (0[,]+∞) ↔ (-𝑒𝑧 ∈ ℝ* ∧ 0 ≀ -𝑒𝑧))
9384, 91, 92sylanbrc 584 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒𝑧 ∈ (0[,]+∞))
9461ffvelcdmi 7083 . . . . . . . . . . . . . 14 (-𝑒𝑧 ∈ (0[,]+∞) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1))
9593, 94syl 17 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1))
9657, 95sselid 3980 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1))
97 iccssre 13403 . . . . . . . . . . . . . . 15 ((-1 ∈ ℝ ∧ 1 ∈ ℝ) β†’ (-1[,]1) βŠ† ℝ)
989, 10, 97mp2an 691 . . . . . . . . . . . . . 14 (-1[,]1) βŠ† ℝ
9998, 96sselid 3980 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ)
100 iccneg 13446 . . . . . . . . . . . . . 14 ((-1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ↔ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1)))
1019, 10, 100mp3an12 1452 . . . . . . . . . . . . 13 ((β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ β†’ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ↔ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1)))
10299, 101syl 17 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ↔ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1)))
10396, 102mpbid 231 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1))
104 negneg1e1 12327 . . . . . . . . . . . 12 --1 = 1
105104oveq2i 7417 . . . . . . . . . . 11 (-1[,]--1) = (-1[,]1)
106103, 105eleqtrdi 2844 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1))
107 xle0neg2 13198 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℝ* β†’ (0 ≀ 𝑧 ↔ -𝑒𝑧 ≀ 0))
108107notbid 318 . . . . . . . . . . . . . 14 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 ↔ Β¬ -𝑒𝑧 ≀ 0))
109108biimpa 478 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ -𝑒𝑧 ≀ 0)
110 f1ocnvfv2 7272 . . . . . . . . . . . . . . 15 ((𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ -𝑒𝑧 ∈ (0[,]+∞)) β†’ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
11121, 93, 110sylancr 588 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
112 0elunit 13443 . . . . . . . . . . . . . . . 16 0 ∈ (0[,]1)
113 ax-1ne0 11176 . . . . . . . . . . . . . . . . . . . . 21 1 β‰  0
114 neeq2 3005 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 0 β†’ (1 β‰  π‘₯ ↔ 1 β‰  0))
115113, 114mpbiri 258 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ 1 β‰  π‘₯)
116115necomd 2997 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 0 β†’ π‘₯ β‰  1)
117 ifnefalse 4540 . . . . . . . . . . . . . . . . . . 19 (π‘₯ β‰  1 β†’ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))) = (π‘₯ / (1 βˆ’ π‘₯)))
118116, 117syl 17 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 0 β†’ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))) = (π‘₯ / (1 βˆ’ π‘₯)))
119 id 22 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ π‘₯ = 0)
120 oveq2 7414 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 0 β†’ (1 βˆ’ π‘₯) = (1 βˆ’ 0))
121 1m0e1 12330 . . . . . . . . . . . . . . . . . . . . 21 (1 βˆ’ 0) = 1
122120, 121eqtrdi 2789 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ (1 βˆ’ π‘₯) = 1)
123119, 122oveq12d 7424 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 0 β†’ (π‘₯ / (1 βˆ’ π‘₯)) = (0 / 1))
124 ax-1cn 11165 . . . . . . . . . . . . . . . . . . . 20 1 ∈ β„‚
125124, 113div0i 11945 . . . . . . . . . . . . . . . . . . 19 (0 / 1) = 0
126123, 125eqtrdi 2789 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 0 β†’ (π‘₯ / (1 βˆ’ π‘₯)) = 0)
127118, 126eqtrd 2773 . . . . . . . . . . . . . . . . 17 (π‘₯ = 0 β†’ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))) = 0)
128 c0ex 11205 . . . . . . . . . . . . . . . . 17 0 ∈ V
129127, 19, 128fvmpt 6996 . . . . . . . . . . . . . . . 16 (0 ∈ (0[,]1) β†’ (πΉβ€˜0) = 0)
130112, 129ax-mp 5 . . . . . . . . . . . . . . 15 (πΉβ€˜0) = 0
131130a1i 11 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜0) = 0)
132111, 131breq12d 5161 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0) ↔ -𝑒𝑧 ≀ 0))
133109, 132mtbird 325 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0))
134 eqid 2733 . . . . . . . . . . . . . . . 16 ((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞)) = ((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞))
13519, 134iccpnfhmeo 24453 . . . . . . . . . . . . . . 15 (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞))))
136135simpli 485 . . . . . . . . . . . . . 14 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137 iccssxr 13404 . . . . . . . . . . . . . . 15 (0[,]1) βŠ† ℝ*
138137, 8pm3.2i 472 . . . . . . . . . . . . . 14 ((0[,]1) βŠ† ℝ* ∧ (0[,]+∞) βŠ† ℝ*)
139 leisorel 14418 . . . . . . . . . . . . . 14 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ((0[,]1) βŠ† ℝ* ∧ (0[,]+∞) βŠ† ℝ*) ∧ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0)))
140136, 138, 139mp3an12 1452 . . . . . . . . . . . . 13 (((β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0)))
14195, 112, 140sylancl 587 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0)))
142133, 141mtbird 325 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ (β—‘πΉβ€˜-𝑒𝑧) ≀ 0)
14399le0neg1d 11782 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
144142, 143mtbid 324 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧))
145 unitssre 13473 . . . . . . . . . . . . . . . . 17 (0[,]1) βŠ† ℝ
146145, 95sselid 3980 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ)
147146recnd 11239 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ β„‚)
148147negnegd 11559 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ --(β—‘πΉβ€˜-𝑒𝑧) = (β—‘πΉβ€˜-𝑒𝑧))
149148fveq2d 6893 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)))
150149, 111eqtrd 2773 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
151 xnegeq 13183 . . . . . . . . . . . 12 ((πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧 β†’ -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒-𝑒𝑧)
152150, 151syl 17 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒-𝑒𝑧)
153 xnegneg 13190 . . . . . . . . . . . 12 (𝑧 ∈ ℝ* β†’ -𝑒-𝑒𝑧 = 𝑧)
154153adantr 482 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒-𝑒𝑧 = 𝑧)
155152, 154eqtr2d 2774 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
156 breq2 5152 . . . . . . . . . . . . 13 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (0 ≀ 𝑦 ↔ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
157156notbid 318 . . . . . . . . . . . 12 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (Β¬ 0 ≀ 𝑦 ↔ Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
158 negeq 11449 . . . . . . . . . . . . . . 15 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ -𝑦 = --(β—‘πΉβ€˜-𝑒𝑧))
159158fveq2d 6893 . . . . . . . . . . . . . 14 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (πΉβ€˜-𝑦) = (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
160 xnegeq 13183 . . . . . . . . . . . . . 14 ((πΉβ€˜-𝑦) = (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
161159, 160syl 17 . . . . . . . . . . . . 13 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
162161eqeq2d 2744 . . . . . . . . . . . 12 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (𝑧 = -𝑒(πΉβ€˜-𝑦) ↔ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧))))
163157, 162anbi12d 632 . . . . . . . . . . 11 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ ((Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) ↔ (Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧) ∧ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))))
164163rspcev 3613 . . . . . . . . . 10 ((-(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ∧ (Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧) ∧ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
165106, 144, 155, 164syl12anc 836 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
166 iffalse 4537 . . . . . . . . . . . 12 (Β¬ 0 ≀ 𝑦 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = -𝑒(πΉβ€˜-𝑦))
167166eqeq2d 2744 . . . . . . . . . . 11 (Β¬ 0 ≀ 𝑦 β†’ (𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ↔ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
168167biimpar 479 . . . . . . . . . 10 ((Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) β†’ 𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
169168reximi 3085 . . . . . . . . 9 (βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
170165, 169syl 17 . . . . . . . 8 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
17182, 170pm2.61dan 812 . . . . . . 7 (𝑧 ∈ ℝ* β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
17250, 171mprgbir 3069 . . . . . 6 ℝ* βŠ† {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))}
1737rnmpt 5953 . . . . . 6 ran 𝐺 = {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))}
174172, 173sseqtrri 4019 . . . . 5 ℝ* βŠ† ran 𝐺
17549, 174eqssi 3998 . . . 4 ran 𝐺 = ℝ*
176 dffo2 6807 . . . 4 (𝐺:(-1[,]1)–onto→ℝ* ↔ (𝐺:(-1[,]1)βŸΆβ„* ∧ ran 𝐺 = ℝ*))
17747, 175, 176mpbir2an 710 . . 3 𝐺:(-1[,]1)–onto→ℝ*
178 breq1 5151 . . . . . . 7 ((πΉβ€˜π‘§) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) β†’ ((πΉβ€˜π‘§) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) ↔ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
179 breq1 5151 . . . . . . 7 (-𝑒(πΉβ€˜-𝑧) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) β†’ (-𝑒(πΉβ€˜-𝑧) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) ↔ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
180 simpl3 1194 . . . . . . . . 9 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 < 𝑀)
181 simpl1 1192 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ (-1[,]1))
182 simpr 486 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 0 ≀ 𝑧)
183 breq2 5152 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ (0 ≀ 𝑦 ↔ 0 ≀ 𝑧))
184 eleq1w 2817 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ (𝑦 ∈ (0[,]1) ↔ 𝑧 ∈ (0[,]1)))
185183, 184imbi12d 345 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ ((0 ≀ 𝑦 β†’ 𝑦 ∈ (0[,]1)) ↔ (0 ≀ 𝑧 β†’ 𝑧 ∈ (0[,]1))))
18618ex 414 . . . . . . . . . . . 12 (𝑦 ∈ (-1[,]1) β†’ (0 ≀ 𝑦 β†’ 𝑦 ∈ (0[,]1)))
187185, 186vtoclga 3566 . . . . . . . . . . 11 (𝑧 ∈ (-1[,]1) β†’ (0 ≀ 𝑧 β†’ 𝑧 ∈ (0[,]1)))
188181, 182, 187sylc 65 . . . . . . . . . 10 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ (0[,]1))
189 simpl2 1193 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑀 ∈ (-1[,]1))
19029a1i 11 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 0 ∈ ℝ)
19198, 181sselid 3980 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ ℝ)
19298, 189sselid 3980 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑀 ∈ ℝ)
193191, 192, 180ltled 11359 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ≀ 𝑀)
194190, 191, 192, 182, 193letrd 11368 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 0 ≀ 𝑀)
195 breq2 5152 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ (0 ≀ 𝑦 ↔ 0 ≀ 𝑀))
196 eleq1w 2817 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ (𝑦 ∈ (0[,]1) ↔ 𝑀 ∈ (0[,]1)))
197195, 196imbi12d 345 . . . . . . . . . . . 12 (𝑦 = 𝑀 β†’ ((0 ≀ 𝑦 β†’ 𝑦 ∈ (0[,]1)) ↔ (0 ≀ 𝑀 β†’ 𝑀 ∈ (0[,]1))))
198197, 186vtoclga 3566 . . . . . . . . . . 11 (𝑀 ∈ (-1[,]1) β†’ (0 ≀ 𝑀 β†’ 𝑀 ∈ (0[,]1)))
199189, 194, 198sylc 65 . . . . . . . . . 10 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑀 ∈ (0[,]1))
200 isorel 7320 . . . . . . . . . . 11 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑀 ∈ (0[,]1))) β†’ (𝑧 < 𝑀 ↔ (πΉβ€˜π‘§) < (πΉβ€˜π‘€)))
201136, 200mpan 689 . . . . . . . . . 10 ((𝑧 ∈ (0[,]1) ∧ 𝑀 ∈ (0[,]1)) β†’ (𝑧 < 𝑀 ↔ (πΉβ€˜π‘§) < (πΉβ€˜π‘€)))
202188, 199, 201syl2anc 585 . . . . . . . . 9 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ (𝑧 < 𝑀 ↔ (πΉβ€˜π‘§) < (πΉβ€˜π‘€)))
203180, 202mpbid 231 . . . . . . . 8 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ (πΉβ€˜π‘§) < (πΉβ€˜π‘€))
204194iftrued 4536 . . . . . . . 8 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) = (πΉβ€˜π‘€))
205203, 204breqtrrd 5176 . . . . . . 7 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ (πΉβ€˜π‘§) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
206 breq2 5152 . . . . . . . 8 ((πΉβ€˜π‘€) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) β†’ (-𝑒(πΉβ€˜-𝑧) < (πΉβ€˜π‘€) ↔ -𝑒(πΉβ€˜-𝑧) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
207 breq2 5152 . . . . . . . 8 (-𝑒(πΉβ€˜-𝑀) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) β†’ (-𝑒(πΉβ€˜-𝑧) < -𝑒(πΉβ€˜-𝑀) ↔ -𝑒(πΉβ€˜-𝑧) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
208 simpl1 1192 . . . . . . . . . . . . . 14 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) β†’ 𝑧 ∈ (-1[,]1))
209 simpr 486 . . . . . . . . . . . . . 14 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ 0 ≀ 𝑧)
210183notbid 318 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 β†’ (Β¬ 0 ≀ 𝑦 ↔ Β¬ 0 ≀ 𝑧))
211 negeq 11449 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 β†’ -𝑦 = -𝑧)
212211eleq1d 2819 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 β†’ (-𝑦 ∈ (0[,]1) ↔ -𝑧 ∈ (0[,]1)))
213210, 212imbi12d 345 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ ((Β¬ 0 ≀ 𝑦 β†’ -𝑦 ∈ (0[,]1)) ↔ (Β¬ 0 ≀ 𝑧 β†’ -𝑧 ∈ (0[,]1))))
21441ex 414 . . . . . . . . . . . . . . 15 (𝑦 ∈ (-1[,]1) β†’ (Β¬ 0 ≀ 𝑦 β†’ -𝑦 ∈ (0[,]1)))
215213, 214vtoclga 3566 . . . . . . . . . . . . . 14 (𝑧 ∈ (-1[,]1) β†’ (Β¬ 0 ≀ 𝑧 β†’ -𝑧 ∈ (0[,]1)))
216208, 209, 215sylc 65 . . . . . . . . . . . . 13 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑧 ∈ (0[,]1))
217216adantr 482 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ -𝑧 ∈ (0[,]1))
21823ffvelcdmi 7083 . . . . . . . . . . . 12 (-𝑧 ∈ (0[,]1) β†’ (πΉβ€˜-𝑧) ∈ (0[,]+∞))
219217, 218syl 17 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ (0[,]+∞))
2208, 219sselid 3980 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ ℝ*)
221220xnegcld 13276 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ -𝑒(πΉβ€˜-𝑧) ∈ ℝ*)
22285a1i 11 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 ∈ ℝ*)
223 simpll2 1214 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑀 ∈ (-1[,]1))
224 simpr 486 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 ≀ 𝑀)
225223, 224, 198sylc 65 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑀 ∈ (0[,]1))
22623ffvelcdmi 7083 . . . . . . . . . . 11 (𝑀 ∈ (0[,]1) β†’ (πΉβ€˜π‘€) ∈ (0[,]+∞))
227225, 226syl 17 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜π‘€) ∈ (0[,]+∞))
2288, 227sselid 3980 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜π‘€) ∈ ℝ*)
229209adantr 482 . . . . . . . . . . . . . 14 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ Β¬ 0 ≀ 𝑧)
230 simpll1 1213 . . . . . . . . . . . . . . . 16 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑧 ∈ (-1[,]1))
23198, 230sselid 3980 . . . . . . . . . . . . . . 15 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑧 ∈ ℝ)
232 ltnle 11290 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 0 ∈ ℝ) β†’ (𝑧 < 0 ↔ Β¬ 0 ≀ 𝑧))
233231, 29, 232sylancl 587 . . . . . . . . . . . . . 14 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (𝑧 < 0 ↔ Β¬ 0 ≀ 𝑧))
234229, 233mpbird 257 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑧 < 0)
235231lt0neg1d 11780 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (𝑧 < 0 ↔ 0 < -𝑧))
236234, 235mpbid 231 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 < -𝑧)
237 isorel 7320 . . . . . . . . . . . . . 14 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) β†’ (0 < -𝑧 ↔ (πΉβ€˜0) < (πΉβ€˜-𝑧)))
238136, 237mpan 689 . . . . . . . . . . . . 13 ((0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) β†’ (0 < -𝑧 ↔ (πΉβ€˜0) < (πΉβ€˜-𝑧)))
239112, 217, 238sylancr 588 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (0 < -𝑧 ↔ (πΉβ€˜0) < (πΉβ€˜-𝑧)))
240236, 239mpbid 231 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜0) < (πΉβ€˜-𝑧))
241130, 240eqbrtrrid 5184 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 < (πΉβ€˜-𝑧))
242 xlt0neg2 13196 . . . . . . . . . . 11 ((πΉβ€˜-𝑧) ∈ ℝ* β†’ (0 < (πΉβ€˜-𝑧) ↔ -𝑒(πΉβ€˜-𝑧) < 0))
243220, 242syl 17 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (0 < (πΉβ€˜-𝑧) ↔ -𝑒(πΉβ€˜-𝑧) < 0))
244241, 243mpbid 231 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ -𝑒(πΉβ€˜-𝑧) < 0)
245 elxrge0 13431 . . . . . . . . . . 11 ((πΉβ€˜π‘€) ∈ (0[,]+∞) ↔ ((πΉβ€˜π‘€) ∈ ℝ* ∧ 0 ≀ (πΉβ€˜π‘€)))
246245simprbi 498 . . . . . . . . . 10 ((πΉβ€˜π‘€) ∈ (0[,]+∞) β†’ 0 ≀ (πΉβ€˜π‘€))
247227, 246syl 17 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 ≀ (πΉβ€˜π‘€))
248221, 222, 228, 244, 247xrltletrd 13137 . . . . . . . 8 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ -𝑒(πΉβ€˜-𝑧) < (πΉβ€˜π‘€))
249 simpll3 1215 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑧 < 𝑀)
250 simpll1 1213 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑧 ∈ (-1[,]1))
25198, 250sselid 3980 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑧 ∈ ℝ)
252 simpll2 1214 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑀 ∈ (-1[,]1))
25398, 252sselid 3980 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑀 ∈ ℝ)
254251, 253ltnegd 11789 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (𝑧 < 𝑀 ↔ -𝑀 < -𝑧))
255249, 254mpbid 231 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ -𝑀 < -𝑧)
256 simpr 486 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ Β¬ 0 ≀ 𝑀)
257195notbid 318 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (Β¬ 0 ≀ 𝑦 ↔ Β¬ 0 ≀ 𝑀))
258 negeq 11449 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 β†’ -𝑦 = -𝑀)
259258eleq1d 2819 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (-𝑦 ∈ (0[,]1) ↔ -𝑀 ∈ (0[,]1)))
260257, 259imbi12d 345 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ ((Β¬ 0 ≀ 𝑦 β†’ -𝑦 ∈ (0[,]1)) ↔ (Β¬ 0 ≀ 𝑀 β†’ -𝑀 ∈ (0[,]1))))
261260, 214vtoclga 3566 . . . . . . . . . . . 12 (𝑀 ∈ (-1[,]1) β†’ (Β¬ 0 ≀ 𝑀 β†’ -𝑀 ∈ (0[,]1)))
262252, 256, 261sylc 65 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ -𝑀 ∈ (0[,]1))
263216adantr 482 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ -𝑧 ∈ (0[,]1))
264 isorel 7320 . . . . . . . . . . . 12 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (-𝑀 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) β†’ (-𝑀 < -𝑧 ↔ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧)))
265136, 264mpan 689 . . . . . . . . . . 11 ((-𝑀 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) β†’ (-𝑀 < -𝑧 ↔ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧)))
266262, 263, 265syl2anc 585 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (-𝑀 < -𝑧 ↔ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧)))
267255, 266mpbid 231 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧))
26823ffvelcdmi 7083 . . . . . . . . . . . 12 (-𝑀 ∈ (0[,]1) β†’ (πΉβ€˜-𝑀) ∈ (0[,]+∞))
269262, 268syl 17 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑀) ∈ (0[,]+∞))
2708, 269sselid 3980 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑀) ∈ ℝ*)
271263, 218syl 17 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ (0[,]+∞))
2728, 271sselid 3980 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ ℝ*)
273 xltneg 13193 . . . . . . . . . 10 (((πΉβ€˜-𝑀) ∈ ℝ* ∧ (πΉβ€˜-𝑧) ∈ ℝ*) β†’ ((πΉβ€˜-𝑀) < (πΉβ€˜-𝑧) ↔ -𝑒(πΉβ€˜-𝑧) < -𝑒(πΉβ€˜-𝑀)))
274270, 272, 273syl2anc 585 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ ((πΉβ€˜-𝑀) < (πΉβ€˜-𝑧) ↔ -𝑒(πΉβ€˜-𝑧) < -𝑒(πΉβ€˜-𝑀)))
275267, 274mpbid 231 . . . . . . . 8 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ -𝑒(πΉβ€˜-𝑧) < -𝑒(πΉβ€˜-𝑀))
276206, 207, 248, 275ifbothda 4566 . . . . . . 7 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒(πΉβ€˜-𝑧) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
277178, 179, 205, 276ifbothda 4566 . . . . . 6 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) β†’ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
2782773expia 1122 . . . . 5 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1)) β†’ (𝑧 < 𝑀 β†’ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
279 fveq2 6889 . . . . . . . 8 (𝑦 = 𝑧 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘§))
280211fveq2d 6893 . . . . . . . . 9 (𝑦 = 𝑧 β†’ (πΉβ€˜-𝑦) = (πΉβ€˜-𝑧))
281 xnegeq 13183 . . . . . . . . 9 ((πΉβ€˜-𝑦) = (πΉβ€˜-𝑧) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑧))
282280, 281syl 17 . . . . . . . 8 (𝑦 = 𝑧 β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑧))
283183, 279, 282ifbieq12d 4556 . . . . . . 7 (𝑦 = 𝑧 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)))
284 fvex 6902 . . . . . . . 8 (πΉβ€˜π‘§) ∈ V
285 xnegex 13184 . . . . . . . 8 -𝑒(πΉβ€˜-𝑧) ∈ V
286284, 285ifex 4578 . . . . . . 7 if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) ∈ V
287283, 7, 286fvmpt 6996 . . . . . 6 (𝑧 ∈ (-1[,]1) β†’ (πΊβ€˜π‘§) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)))
288 fveq2 6889 . . . . . . . 8 (𝑦 = 𝑀 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘€))
289258fveq2d 6893 . . . . . . . . 9 (𝑦 = 𝑀 β†’ (πΉβ€˜-𝑦) = (πΉβ€˜-𝑀))
290 xnegeq 13183 . . . . . . . . 9 ((πΉβ€˜-𝑦) = (πΉβ€˜-𝑀) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑀))
291289, 290syl 17 . . . . . . . 8 (𝑦 = 𝑀 β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑀))
292195, 288, 291ifbieq12d 4556 . . . . . . 7 (𝑦 = 𝑀 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
293 fvex 6902 . . . . . . . 8 (πΉβ€˜π‘€) ∈ V
294 xnegex 13184 . . . . . . . 8 -𝑒(πΉβ€˜-𝑀) ∈ V
295293, 294ifex 4578 . . . . . . 7 if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) ∈ V
296292, 7, 295fvmpt 6996 . . . . . 6 (𝑀 ∈ (-1[,]1) β†’ (πΊβ€˜π‘€) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
297287, 296breqan12d 5164 . . . . 5 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1)) β†’ ((πΊβ€˜π‘§) < (πΊβ€˜π‘€) ↔ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
298278, 297sylibrd 259 . . . 4 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1)) β†’ (𝑧 < 𝑀 β†’ (πΊβ€˜π‘§) < (πΊβ€˜π‘€)))
299298rgen2 3198 . . 3 βˆ€π‘§ ∈ (-1[,]1)βˆ€π‘€ ∈ (-1[,]1)(𝑧 < 𝑀 β†’ (πΊβ€˜π‘§) < (πΊβ€˜π‘€))
300 soisoi 7322 . . 3 ((( < Or (-1[,]1) ∧ < Po ℝ*) ∧ (𝐺:(-1[,]1)–onto→ℝ* ∧ βˆ€π‘§ ∈ (-1[,]1)βˆ€π‘€ ∈ (-1[,]1)(𝑧 < 𝑀 β†’ (πΊβ€˜π‘§) < (πΊβ€˜π‘€)))) β†’ 𝐺 Isom < , < ((-1[,]1), ℝ*))
3014, 6, 177, 299, 300mp4an 692 . 2 𝐺 Isom < , < ((-1[,]1), ℝ*)
302 letsr 18543 . . . . . 6 ≀ ∈ TosetRel
303302elexi 3494 . . . . 5 ≀ ∈ V
304303inex1 5317 . . . 4 ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) ∈ V
305 ssid 4004 . . . . . . 7 ℝ* βŠ† ℝ*
306 leiso 14417 . . . . . . 7 (((-1[,]1) βŠ† ℝ* ∧ ℝ* βŠ† ℝ*) β†’ (𝐺 Isom < , < ((-1[,]1), ℝ*) ↔ 𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*)))
3071, 305, 306mp2an 691 . . . . . 6 (𝐺 Isom < , < ((-1[,]1), ℝ*) ↔ 𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*))
308301, 307mpbi 229 . . . . 5 𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*)
309 isores1 7328 . . . . 5 (𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*) ↔ 𝐺 Isom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))), ≀ ((-1[,]1), ℝ*))
310308, 309mpbi 229 . . . 4 𝐺 Isom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))), ≀ ((-1[,]1), ℝ*)
311 tsrps 18537 . . . . . . . 8 ( ≀ ∈ TosetRel β†’ ≀ ∈ PosetRel)
312302, 311ax-mp 5 . . . . . . 7 ≀ ∈ PosetRel
313 ledm 18540 . . . . . . . 8 ℝ* = dom ≀
314313psssdm 18532 . . . . . . 7 (( ≀ ∈ PosetRel ∧ (-1[,]1) βŠ† ℝ*) β†’ dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) = (-1[,]1))
315312, 1, 314mp2an 691 . . . . . 6 dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) = (-1[,]1)
316315eqcomi 2742 . . . . 5 (-1[,]1) = dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1)))
317316, 313ordthmeo 23298 . . . 4 ((( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) ∈ V ∧ ≀ ∈ TosetRel ∧ 𝐺 Isom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))), ≀ ((-1[,]1), ℝ*)) β†’ 𝐺 ∈ ((ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))Homeo(ordTopβ€˜ ≀ )))
318304, 302, 310, 317mp3an 1462 . . 3 𝐺 ∈ ((ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))Homeo(ordTopβ€˜ ≀ ))
319 xrhmeo.j . . . . . . 7 𝐽 = (TopOpenβ€˜β„‚fld)
320 eqid 2733 . . . . . . 7 (ordTopβ€˜ ≀ ) = (ordTopβ€˜ ≀ )
321319, 320xrrest2 24316 . . . . . 6 ((-1[,]1) βŠ† ℝ β†’ (𝐽 β†Ύt (-1[,]1)) = ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1)))
32298, 321ax-mp 5 . . . . 5 (𝐽 β†Ύt (-1[,]1)) = ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1))
323 ordtresticc 22719 . . . . 5 ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1)) = (ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))
324322, 323eqtri 2761 . . . 4 (𝐽 β†Ύt (-1[,]1)) = (ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))
325324oveq1i 7416 . . 3 ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ )) = ((ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))Homeo(ordTopβ€˜ ≀ ))
326318, 325eleqtrri 2833 . 2 𝐺 ∈ ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ ))
327301, 326pm3.2i 472 1 (𝐺 Isom < , < ((-1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ )))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   ∩ cin 3947   βŠ† wss 3948  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231   Po wpo 5586   Or wor 5587   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677  βŸΆwf 6537  β€“ontoβ†’wfo 6539  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541   Isom wiso 6542  (class class class)co 7406  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110  +∞cpnf 11242  β„*cxr 11244   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441  -cneg 11442   / cdiv 11868  -𝑒cxne 13086  [,]cicc 13324   β†Ύt crest 17363  TopOpenctopn 17364  ordTopcordt 17442  PosetRelcps 18514   TosetRel ctsr 18515  β„‚fldccnfld 20937  Homeochmeo 23249  IIcii 24383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fi 9403  df-sup 9434  df-inf 9435  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-struct 17077  df-slot 17112  df-ndx 17124  df-base 17142  df-plusg 17207  df-mulr 17208  df-starv 17209  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-rest 17365  df-topn 17366  df-topgen 17386  df-ordt 17444  df-ps 18516  df-tsr 18517  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cn 22723  df-hmeo 23251  df-xms 23818  df-ms 23819  df-ii 24385
This theorem is referenced by:  xrhmph  24455
  Copyright terms: Public domain W3C validator