MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrhmeo Structured version   Visualization version   GIF version
Theorem xrhmeo 24791
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 13414 . . . 4 (-1[,]1) βŠ† ℝ*
2 xrltso 13127 . . . 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 13414 . . . . . . 7 (0[,]+∞) βŠ† ℝ*
9 neg1rr 12334 . . . . . . . . . . . 12 -1 ∈ ℝ
10 1re 11221 . . . . . . . . . . . 12 1 ∈ ℝ
119, 10elicc2i 13397 . . . . . . . . . . 11 (𝑦 ∈ (-1[,]1) ↔ (𝑦 ∈ ℝ ∧ -1 ≀ 𝑦 ∧ 𝑦 ≀ 1))
1211simp1bi 1144 . . . . . . . . . 10 (𝑦 ∈ (-1[,]1) β†’ 𝑦 ∈ ℝ)
1312adantr 480 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 𝑦 ∈ ℝ)
14 simpr 484 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 0 ≀ 𝑦)
1511simp3bi 1146 . . . . . . . . . 10 (𝑦 ∈ (-1[,]1) β†’ 𝑦 ≀ 1)
1615adantr 480 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 𝑦 ≀ 1)
17 elicc01 13450 . . . . . . . . 9 (𝑦 ∈ (0[,]1) ↔ (𝑦 ∈ ℝ ∧ 0 ≀ 𝑦 ∧ 𝑦 ≀ 1))
1813, 14, 16, 17syl3anbrc 1342 . . . . . . . 8 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ 𝑦 ∈ (0[,]1))
19 xrhmeo.f . . . . . . . . . . . 12 𝐹 = (π‘₯ ∈ (0[,]1) ↦ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))))
2019iccpnfcnv 24789 . . . . . . . . . . 11 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ ◑𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
2120simpli 483 . . . . . . . . . 10 𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞)
22 f1of 6833 . . . . . . . . . 10 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) β†’ 𝐹:(0[,]1)⟢(0[,]+∞))
2321, 22ax-mp 5 . . . . . . . . 9 𝐹:(0[,]1)⟢(0[,]+∞)
2423ffvelcdmi 7085 . . . . . . . 8 (𝑦 ∈ (0[,]1) β†’ (πΉβ€˜π‘¦) ∈ (0[,]+∞))
2518, 24syl 17 . . . . . . 7 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ (πΉβ€˜π‘¦) ∈ (0[,]+∞))
268, 25sselid 3980 . . . . . 6 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ (πΉβ€˜π‘¦) ∈ ℝ*)
2712adantr 480 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 𝑦 ∈ ℝ)
2827renegcld 11648 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ∈ ℝ)
29 0re 11223 . . . . . . . . . . . . 13 0 ∈ ℝ
30 letric 11321 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (0 ≀ 𝑦 ∨ 𝑦 ≀ 0))
3129, 12, 30sylancr 586 . . . . . . . . . . . 12 (𝑦 ∈ (-1[,]1) β†’ (0 ≀ 𝑦 ∨ 𝑦 ≀ 0))
3231orcanai 1000 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 𝑦 ≀ 0)
3327le0neg1d 11792 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (𝑦 ≀ 0 ↔ 0 ≀ -𝑦))
3432, 33mpbid 231 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 0 ≀ -𝑦)
3511simp2bi 1145 . . . . . . . . . . . 12 (𝑦 ∈ (-1[,]1) β†’ -1 ≀ 𝑦)
3635adantr 480 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -1 ≀ 𝑦)
37 lenegcon1 11725 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (-1 ≀ 𝑦 ↔ -𝑦 ≀ 1))
3810, 27, 37sylancr 586 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (-1 ≀ 𝑦 ↔ -𝑦 ≀ 1))
3936, 38mpbid 231 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ≀ 1)
40 elicc01 13450 . . . . . . . . . 10 (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≀ -𝑦 ∧ -𝑦 ≀ 1))
4128, 34, 39, 40syl3anbrc 1342 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ∈ (0[,]1))
4223ffvelcdmi 7085 . . . . . . . . 9 (-𝑦 ∈ (0[,]1) β†’ (πΉβ€˜-𝑦) ∈ (0[,]+∞))
4341, 42syl 17 . . . . . . . 8 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (πΉβ€˜-𝑦) ∈ (0[,]+∞))
448, 43sselid 3980 . . . . . . 7 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (πΉβ€˜-𝑦) ∈ ℝ*)
4544xnegcld 13286 . . . . . 6 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑒(πΉβ€˜-𝑦) ∈ ℝ*)
4626, 45ifclda 4563 . . . . 5 (𝑦 ∈ (-1[,]1) β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ∈ ℝ*)
477, 46fmpti 7113 . . . 4 𝐺:(-1[,]1)βŸΆβ„*
48 frn 6724 . . . . . 6 (𝐺:(-1[,]1)βŸΆβ„* β†’ ran 𝐺 βŠ† ℝ*)
4947, 48ax-mp 5 . . . . 5 ran 𝐺 βŠ† ℝ*
50 ssabral 4059 . . . . . . 7 (ℝ* βŠ† {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))} ↔ βˆ€π‘§ ∈ ℝ* βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
51 0le1 11744 . . . . . . . . . . . . 13 0 ≀ 1
52 le0neg2 11730 . . . . . . . . . . . . . 14 (1 ∈ ℝ β†’ (0 ≀ 1 ↔ -1 ≀ 0))
5310, 52ax-mp 5 . . . . . . . . . . . . 13 (0 ≀ 1 ↔ -1 ≀ 0)
5451, 53mpbi 229 . . . . . . . . . . . 12 -1 ≀ 0
55 1le1 11849 . . . . . . . . . . . 12 1 ≀ 1
56 iccss 13399 . . . . . . . . . . . 12 (((-1 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (-1 ≀ 0 ∧ 1 ≀ 1)) β†’ (0[,]1) βŠ† (-1[,]1))
579, 10, 54, 55, 56mp4an 690 . . . . . . . . . . 11 (0[,]1) βŠ† (-1[,]1)
58 elxrge0 13441 . . . . . . . . . . . 12 (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧))
59 f1ocnv 6845 . . . . . . . . . . . . . 14 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) β†’ ◑𝐹:(0[,]+∞)–1-1-ontoβ†’(0[,]1))
60 f1of 6833 . . . . . . . . . . . . . 14 (◑𝐹:(0[,]+∞)–1-1-ontoβ†’(0[,]1) β†’ ◑𝐹:(0[,]+∞)⟢(0[,]1))
6121, 59, 60mp2b 10 . . . . . . . . . . . . 13 ◑𝐹:(0[,]+∞)⟢(0[,]1)
6261ffvelcdmi 7085 . . . . . . . . . . . 12 (𝑧 ∈ (0[,]+∞) β†’ (β—‘πΉβ€˜π‘§) ∈ (0[,]1))
6358, 62sylbir 234 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜π‘§) ∈ (0[,]1))
6457, 63sselid 3980 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜π‘§) ∈ (-1[,]1))
65 elicc01 13450 . . . . . . . . . . . 12 ((β—‘πΉβ€˜π‘§) ∈ (0[,]1) ↔ ((β—‘πΉβ€˜π‘§) ∈ ℝ ∧ 0 ≀ (β—‘πΉβ€˜π‘§) ∧ (β—‘πΉβ€˜π‘§) ≀ 1))
6665simp2bi 1145 . . . . . . . . . . 11 ((β—‘πΉβ€˜π‘§) ∈ (0[,]1) β†’ 0 ≀ (β—‘πΉβ€˜π‘§))
6763, 66syl 17 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 0 ≀ (β—‘πΉβ€˜π‘§))
6858biimpri 227 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ (0[,]+∞))
69 f1ocnvfv2 7278 . . . . . . . . . . . 12 ((𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘§)) = 𝑧)
7021, 68, 69sylancr 586 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘§)) = 𝑧)
7170eqcomd 2737 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))
72 breq2 5152 . . . . . . . . . . . 12 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (0 ≀ 𝑦 ↔ 0 ≀ (β—‘πΉβ€˜π‘§)))
73 fveq2 6891 . . . . . . . . . . . . 13 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜(β—‘πΉβ€˜π‘§)))
7473eqeq2d 2742 . . . . . . . . . . . 12 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (𝑧 = (πΉβ€˜π‘¦) ↔ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§))))
7572, 74anbi12d 630 . . . . . . . . . . 11 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ ((0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) ↔ (0 ≀ (β—‘πΉβ€˜π‘§) ∧ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))))
7675rspcev 3612 . . . . . . . . . 10 (((β—‘πΉβ€˜π‘§) ∈ (-1[,]1) ∧ (0 ≀ (β—‘πΉβ€˜π‘§) ∧ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)))
7764, 67, 71, 76syl12anc 834 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)))
78 iftrue 4534 . . . . . . . . . . . 12 (0 ≀ 𝑦 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = (πΉβ€˜π‘¦))
7978eqeq2d 2742 . . . . . . . . . . 11 (0 ≀ 𝑦 β†’ (𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ↔ 𝑧 = (πΉβ€˜π‘¦)))
8079biimpar 477 . . . . . . . . . 10 ((0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) β†’ 𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8180reximi 3083 . . . . . . . . 9 (βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8277, 81syl 17 . . . . . . . 8 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
83 xnegcl 13199 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℝ* β†’ -𝑒𝑧 ∈ ℝ*)
8483adantr 480 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒𝑧 ∈ ℝ*)
85 0xr 11268 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ*
86 xrletri 13139 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) β†’ (0 ≀ 𝑧 ∨ 𝑧 ≀ 0))
8785, 86mpan 687 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℝ* β†’ (0 ≀ 𝑧 ∨ 𝑧 ≀ 0))
8887ord 861 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 β†’ 𝑧 ≀ 0))
89 xle0neg1 13207 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℝ* β†’ (𝑧 ≀ 0 ↔ 0 ≀ -𝑒𝑧))
9088, 89sylibd 238 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 β†’ 0 ≀ -𝑒𝑧))
9190imp 406 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ 0 ≀ -𝑒𝑧)
92 elxrge0 13441 . . . . . . . . . . . . . . 15 (-𝑒𝑧 ∈ (0[,]+∞) ↔ (-𝑒𝑧 ∈ ℝ* ∧ 0 ≀ -𝑒𝑧))
9384, 91, 92sylanbrc 582 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒𝑧 ∈ (0[,]+∞))
9461ffvelcdmi 7085 . . . . . . . . . . . . . 14 (-𝑒𝑧 ∈ (0[,]+∞) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1))
9593, 94syl 17 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1))
9657, 95sselid 3980 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1))
97 iccssre 13413 . . . . . . . . . . . . . . 15 ((-1 ∈ ℝ ∧ 1 ∈ ℝ) β†’ (-1[,]1) βŠ† ℝ)
989, 10, 97mp2an 689 . . . . . . . . . . . . . 14 (-1[,]1) βŠ† ℝ
9998, 96sselid 3980 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ)
100 iccneg 13456 . . . . . . . . . . . . . 14 ((-1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ↔ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1)))
1019, 10, 100mp3an12 1450 . . . . . . . . . . . . 13 ((β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ β†’ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ↔ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1)))
10299, 101syl 17 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ↔ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1)))
10396, 102mpbid 231 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]--1))
104 negneg1e1 12337 . . . . . . . . . . . 12 --1 = 1
105104oveq2i 7423 . . . . . . . . . . 11 (-1[,]--1) = (-1[,]1)
106103, 105eleqtrdi 2842 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1))
107 xle0neg2 13208 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℝ* β†’ (0 ≀ 𝑧 ↔ -𝑒𝑧 ≀ 0))
108107notbid 318 . . . . . . . . . . . . . 14 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 ↔ Β¬ -𝑒𝑧 ≀ 0))
109108biimpa 476 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ -𝑒𝑧 ≀ 0)
110 f1ocnvfv2 7278 . . . . . . . . . . . . . . 15 ((𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ -𝑒𝑧 ∈ (0[,]+∞)) β†’ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
11121, 93, 110sylancr 586 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
112 0elunit 13453 . . . . . . . . . . . . . . . 16 0 ∈ (0[,]1)
113 ax-1ne0 11185 . . . . . . . . . . . . . . . . . . . . 21 1 β‰  0
114 neeq2 3003 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 0 β†’ (1 β‰  π‘₯ ↔ 1 β‰  0))
115113, 114mpbiri 258 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ 1 β‰  π‘₯)
116115necomd 2995 . . . . . . . . . . . . . . . . . . 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 7420 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 0 β†’ (1 βˆ’ π‘₯) = (1 βˆ’ 0))
121 1m0e1 12340 . . . . . . . . . . . . . . . . . . . . 21 (1 βˆ’ 0) = 1
122120, 121eqtrdi 2787 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ (1 βˆ’ π‘₯) = 1)
123119, 122oveq12d 7430 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 0 β†’ (π‘₯ / (1 βˆ’ π‘₯)) = (0 / 1))
124 ax-1cn 11174 . . . . . . . . . . . . . . . . . . . 20 1 ∈ β„‚
125124, 113div0i 11955 . . . . . . . . . . . . . . . . . . 19 (0 / 1) = 0
126123, 125eqtrdi 2787 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 0 β†’ (π‘₯ / (1 βˆ’ π‘₯)) = 0)
127118, 126eqtrd 2771 . . . . . . . . . . . . . . . . 17 (π‘₯ = 0 β†’ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))) = 0)
128 c0ex 11215 . . . . . . . . . . . . . . . . 17 0 ∈ V
129127, 19, 128fvmpt 6998 . . . . . . . . . . . . . . . 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 2731 . . . . . . . . . . . . . . . 16 ((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞)) = ((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞))
13519, 134iccpnfhmeo 24790 . . . . . . . . . . . . . . 15 (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞))))
136135simpli 483 . . . . . . . . . . . . . 14 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137 iccssxr 13414 . . . . . . . . . . . . . . 15 (0[,]1) βŠ† ℝ*
138137, 8pm3.2i 470 . . . . . . . . . . . . . 14 ((0[,]1) βŠ† ℝ* ∧ (0[,]+∞) βŠ† ℝ*)
139 leisorel 14428 . . . . . . . . . . . . . 14 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ((0[,]1) βŠ† ℝ* ∧ (0[,]+∞) βŠ† ℝ*) ∧ ((β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0)))
140136, 138, 139mp3an12 1450 . . . . . . . . . . . . 13 (((β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0)))
14195, 112, 140sylancl 585 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0)))
142133, 141mtbird 325 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ (β—‘πΉβ€˜-𝑒𝑧) ≀ 0)
14399le0neg1d 11792 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
144142, 143mtbid 324 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧))
145 unitssre 13483 . . . . . . . . . . . . . . . . 17 (0[,]1) βŠ† ℝ
146145, 95sselid 3980 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ)
147146recnd 11249 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ β„‚)
148147negnegd 11569 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ --(β—‘πΉβ€˜-𝑒𝑧) = (β—‘πΉβ€˜-𝑒𝑧))
149148fveq2d 6895 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)))
150149, 111eqtrd 2771 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
151 xnegeq 13193 . . . . . . . . . . . 12 ((πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧 β†’ -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒-𝑒𝑧)
152150, 151syl 17 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒-𝑒𝑧)
153 xnegneg 13200 . . . . . . . . . . . 12 (𝑧 ∈ ℝ* β†’ -𝑒-𝑒𝑧 = 𝑧)
154153adantr 480 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒-𝑒𝑧 = 𝑧)
155152, 154eqtr2d 2772 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
156 breq2 5152 . . . . . . . . . . . . 13 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (0 ≀ 𝑦 ↔ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
157156notbid 318 . . . . . . . . . . . 12 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (Β¬ 0 ≀ 𝑦 ↔ Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
158 negeq 11459 . . . . . . . . . . . . . . 15 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ -𝑦 = --(β—‘πΉβ€˜-𝑒𝑧))
159158fveq2d 6895 . . . . . . . . . . . . . 14 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (πΉβ€˜-𝑦) = (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
160 xnegeq 13193 . . . . . . . . . . . . . 14 ((πΉβ€˜-𝑦) = (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
161159, 160syl 17 . . . . . . . . . . . . 13 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
162161eqeq2d 2742 . . . . . . . . . . . 12 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (𝑧 = -𝑒(πΉβ€˜-𝑦) ↔ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧))))
163157, 162anbi12d 630 . . . . . . . . . . 11 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ ((Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) ↔ (Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧) ∧ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))))
164163rspcev 3612 . . . . . . . . . 10 ((-(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ∧ (Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧) ∧ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
165106, 144, 155, 164syl12anc 834 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
166 iffalse 4537 . . . . . . . . . . . 12 (Β¬ 0 ≀ 𝑦 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = -𝑒(πΉβ€˜-𝑦))
167166eqeq2d 2742 . . . . . . . . . . 11 (Β¬ 0 ≀ 𝑦 β†’ (𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ↔ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
168167biimpar 477 . . . . . . . . . 10 ((Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) β†’ 𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
169168reximi 3083 . . . . . . . . 9 (βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
170165, 169syl 17 . . . . . . . 8 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
17182, 170pm2.61dan 810 . . . . . . 7 (𝑧 ∈ ℝ* β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
17250, 171mprgbir 3067 . . . . . 6 ℝ* βŠ† {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))}
1737rnmpt 5954 . . . . . 6 ran 𝐺 = {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))}
174172, 173sseqtrri 4019 . . . . 5 ℝ* βŠ† ran 𝐺
17549, 174eqssi 3998 . . . 4 ran 𝐺 = ℝ*
176 dffo2 6809 . . . 4 (𝐺:(-1[,]1)–onto→ℝ* ↔ (𝐺:(-1[,]1)βŸΆβ„* ∧ ran 𝐺 = ℝ*))
17747, 175, 176mpbir2an 708 . . 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 1192 . . . . . . . . 9 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 < 𝑀)
181 simpl1 1190 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ (-1[,]1))
182 simpr 484 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 0 ≀ 𝑧)
183 breq2 5152 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ (0 ≀ 𝑦 ↔ 0 ≀ 𝑧))
184 eleq1w 2815 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ (𝑦 ∈ (0[,]1) ↔ 𝑧 ∈ (0[,]1)))
185183, 184imbi12d 344 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ ((0 ≀ 𝑦 β†’ 𝑦 ∈ (0[,]1)) ↔ (0 ≀ 𝑧 β†’ 𝑧 ∈ (0[,]1))))
18618ex 412 . . . . . . . . . . . 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 1191 . . . . . . . . . . 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 11369 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ≀ 𝑀)
194190, 191, 192, 182, 193letrd 11378 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 0 ≀ 𝑀)
195 breq2 5152 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ (0 ≀ 𝑦 ↔ 0 ≀ 𝑀))
196 eleq1w 2815 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ (𝑦 ∈ (0[,]1) ↔ 𝑀 ∈ (0[,]1)))
197195, 196imbi12d 344 . . . . . . . . . . . 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 7326 . . . . . . . . . . 11 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑀 ∈ (0[,]1))) β†’ (𝑧 < 𝑀 ↔ (πΉβ€˜π‘§) < (πΉβ€˜π‘€)))
201136, 200mpan 687 . . . . . . . . . 10 ((𝑧 ∈ (0[,]1) ∧ 𝑀 ∈ (0[,]1)) β†’ (𝑧 < 𝑀 ↔ (πΉβ€˜π‘§) < (πΉβ€˜π‘€)))
202188, 199, 201syl2anc 583 . . . . . . . . 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 1190 . . . . . . . . . . . . . 14 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) β†’ 𝑧 ∈ (-1[,]1))
209 simpr 484 . . . . . . . . . . . . . 14 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ 0 ≀ 𝑧)
210183notbid 318 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 β†’ (Β¬ 0 ≀ 𝑦 ↔ Β¬ 0 ≀ 𝑧))
211 negeq 11459 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 β†’ -𝑦 = -𝑧)
212211eleq1d 2817 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 β†’ (-𝑦 ∈ (0[,]1) ↔ -𝑧 ∈ (0[,]1)))
213210, 212imbi12d 344 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ ((Β¬ 0 ≀ 𝑦 β†’ -𝑦 ∈ (0[,]1)) ↔ (Β¬ 0 ≀ 𝑧 β†’ -𝑧 ∈ (0[,]1))))
21441ex 412 . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ -𝑧 ∈ (0[,]1))
21823ffvelcdmi 7085 . . . . . . . . . . . 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 13286 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ -𝑒(πΉβ€˜-𝑧) ∈ ℝ*)
22285a1i 11 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 ∈ ℝ*)
223 simpll2 1212 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑀 ∈ (-1[,]1))
224 simpr 484 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 ≀ 𝑀)
225223, 224, 198sylc 65 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑀 ∈ (0[,]1))
22623ffvelcdmi 7085 . . . . . . . . . . 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 480 . . . . . . . . . . . . . 14 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ Β¬ 0 ≀ 𝑧)
230 simpll1 1211 . . . . . . . . . . . . . . . 16 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑧 ∈ (-1[,]1))
23198, 230sselid 3980 . . . . . . . . . . . . . . 15 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑧 ∈ ℝ)
232 ltnle 11300 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 0 ∈ ℝ) β†’ (𝑧 < 0 ↔ Β¬ 0 ≀ 𝑧))
233231, 29, 232sylancl 585 . . . . . . . . . . . . . 14 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (𝑧 < 0 ↔ Β¬ 0 ≀ 𝑧))
234229, 233mpbird 257 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑧 < 0)
235231lt0neg1d 11790 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (𝑧 < 0 ↔ 0 < -𝑧))
236234, 235mpbid 231 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 < -𝑧)
237 isorel 7326 . . . . . . . . . . . . . 14 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) β†’ (0 < -𝑧 ↔ (πΉβ€˜0) < (πΉβ€˜-𝑧)))
238136, 237mpan 687 . . . . . . . . . . . . 13 ((0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) β†’ (0 < -𝑧 ↔ (πΉβ€˜0) < (πΉβ€˜-𝑧)))
239112, 217, 238sylancr 586 . . . . . . . . . . . 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 13206 . . . . . . . . . . 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 13441 . . . . . . . . . . 11 ((πΉβ€˜π‘€) ∈ (0[,]+∞) ↔ ((πΉβ€˜π‘€) ∈ ℝ* ∧ 0 ≀ (πΉβ€˜π‘€)))
246245simprbi 496 . . . . . . . . . 10 ((πΉβ€˜π‘€) ∈ (0[,]+∞) β†’ 0 ≀ (πΉβ€˜π‘€))
247227, 246syl 17 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 ≀ (πΉβ€˜π‘€))
248221, 222, 228, 244, 247xrltletrd 13147 . . . . . . . 8 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ -𝑒(πΉβ€˜-𝑧) < (πΉβ€˜π‘€))
249 simpll3 1213 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑧 < 𝑀)
250 simpll1 1211 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑧 ∈ (-1[,]1))
25198, 250sselid 3980 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑧 ∈ ℝ)
252 simpll2 1212 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑀 ∈ (-1[,]1))
25398, 252sselid 3980 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑀 ∈ ℝ)
254251, 253ltnegd 11799 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (𝑧 < 𝑀 ↔ -𝑀 < -𝑧))
255249, 254mpbid 231 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ -𝑀 < -𝑧)
256 simpr 484 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ Β¬ 0 ≀ 𝑀)
257195notbid 318 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (Β¬ 0 ≀ 𝑦 ↔ Β¬ 0 ≀ 𝑀))
258 negeq 11459 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 β†’ -𝑦 = -𝑀)
259258eleq1d 2817 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (-𝑦 ∈ (0[,]1) ↔ -𝑀 ∈ (0[,]1)))
260257, 259imbi12d 344 . . . . . . . . . . . . 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 480 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ -𝑧 ∈ (0[,]1))
264 isorel 7326 . . . . . . . . . . . 12 ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (-𝑀 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) β†’ (-𝑀 < -𝑧 ↔ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧)))
265136, 264mpan 687 . . . . . . . . . . 11 ((-𝑀 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) β†’ (-𝑀 < -𝑧 ↔ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧)))
266262, 263, 265syl2anc 583 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (-𝑀 < -𝑧 ↔ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧)))
267255, 266mpbid 231 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑀) < (πΉβ€˜-𝑧))
26823ffvelcdmi 7085 . . . . . . . . . . . 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 13203 . . . . . . . . . 10 (((πΉβ€˜-𝑀) ∈ ℝ* ∧ (πΉβ€˜-𝑧) ∈ ℝ*) β†’ ((πΉβ€˜-𝑀) < (πΉβ€˜-𝑧) ↔ -𝑒(πΉβ€˜-𝑧) < -𝑒(πΉβ€˜-𝑀)))
274270, 272, 273syl2anc 583 . . . . . . . . 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 1120 . . . . 5 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1)) β†’ (𝑧 < 𝑀 β†’ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
279 fveq2 6891 . . . . . . . 8 (𝑦 = 𝑧 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘§))
280211fveq2d 6895 . . . . . . . . 9 (𝑦 = 𝑧 β†’ (πΉβ€˜-𝑦) = (πΉβ€˜-𝑧))
281 xnegeq 13193 . . . . . . . . 9 ((πΉβ€˜-𝑦) = (πΉβ€˜-𝑧) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑧))
282280, 281syl 17 . . . . . . . 8 (𝑦 = 𝑧 β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑧))
283183, 279, 282ifbieq12d 4556 . . . . . . 7 (𝑦 = 𝑧 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)))
284 fvex 6904 . . . . . . . 8 (πΉβ€˜π‘§) ∈ V
285 xnegex 13194 . . . . . . . 8 -𝑒(πΉβ€˜-𝑧) ∈ V
286284, 285ifex 4578 . . . . . . 7 if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) ∈ V
287283, 7, 286fvmpt 6998 . . . . . 6 (𝑧 ∈ (-1[,]1) β†’ (πΊβ€˜π‘§) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)))
288 fveq2 6891 . . . . . . . 8 (𝑦 = 𝑀 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘€))
289258fveq2d 6895 . . . . . . . . 9 (𝑦 = 𝑀 β†’ (πΉβ€˜-𝑦) = (πΉβ€˜-𝑀))
290 xnegeq 13193 . . . . . . . . 9 ((πΉβ€˜-𝑦) = (πΉβ€˜-𝑀) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑀))
291289, 290syl 17 . . . . . . . 8 (𝑦 = 𝑀 β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑀))
292195, 288, 291ifbieq12d 4556 . . . . . . 7 (𝑦 = 𝑀 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
293 fvex 6904 . . . . . . . 8 (πΉβ€˜π‘€) ∈ V
294 xnegex 13194 . . . . . . . 8 -𝑒(πΉβ€˜-𝑀) ∈ V
295293, 294ifex 4578 . . . . . . 7 if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) ∈ V
296292, 7, 295fvmpt 6998 . . . . . 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 3196 . . 3 βˆ€π‘§ ∈ (-1[,]1)βˆ€π‘€ ∈ (-1[,]1)(𝑧 < 𝑀 β†’ (πΊβ€˜π‘§) < (πΊβ€˜π‘€))
300 soisoi 7328 . . 3 ((( < Or (-1[,]1) ∧ < Po ℝ*) ∧ (𝐺:(-1[,]1)–onto→ℝ* ∧ βˆ€π‘§ ∈ (-1[,]1)βˆ€π‘€ ∈ (-1[,]1)(𝑧 < 𝑀 β†’ (πΊβ€˜π‘§) < (πΊβ€˜π‘€)))) β†’ 𝐺 Isom < , < ((-1[,]1), ℝ*))
3014, 6, 177, 299, 300mp4an 690 . 2 𝐺 Isom < , < ((-1[,]1), ℝ*)
302 letsr 18556 . . . . . 6 ≀ ∈ TosetRel
303302elexi 3493 . . . . 5 ≀ ∈ V
304303inex1 5317 . . . 4 ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) ∈ V
305 ssid 4004 . . . . . . 7 ℝ* βŠ† ℝ*
306 leiso 14427 . . . . . . 7 (((-1[,]1) βŠ† ℝ* ∧ ℝ* βŠ† ℝ*) β†’ (𝐺 Isom < , < ((-1[,]1), ℝ*) ↔ 𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*)))
3071, 305, 306mp2an 689 . . . . . 6 (𝐺 Isom < , < ((-1[,]1), ℝ*) ↔ 𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*))
308301, 307mpbi 229 . . . . 5 𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*)
309 isores1 7334 . . . . 5 (𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*) ↔ 𝐺 Isom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))), ≀ ((-1[,]1), ℝ*))
310308, 309mpbi 229 . . . 4 𝐺 Isom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))), ≀ ((-1[,]1), ℝ*)
311 tsrps 18550 . . . . . . . 8 ( ≀ ∈ TosetRel β†’ ≀ ∈ PosetRel)
312302, 311ax-mp 5 . . . . . . 7 ≀ ∈ PosetRel
313 ledm 18553 . . . . . . . 8 ℝ* = dom ≀
314313psssdm 18545 . . . . . . 7 (( ≀ ∈ PosetRel ∧ (-1[,]1) βŠ† ℝ*) β†’ dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) = (-1[,]1))
315312, 1, 314mp2an 689 . . . . . 6 dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) = (-1[,]1)
316315eqcomi 2740 . . . . 5 (-1[,]1) = dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1)))
317316, 313ordthmeo 23626 . . . 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 1460 . . 3 𝐺 ∈ ((ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))Homeo(ordTopβ€˜ ≀ ))
319 xrhmeo.j . . . . . . 7 𝐽 = (TopOpenβ€˜β„‚fld)
320 eqid 2731 . . . . . . 7 (ordTopβ€˜ ≀ ) = (ordTopβ€˜ ≀ )
321319, 320xrrest2 24644 . . . . . 6 ((-1[,]1) βŠ† ℝ β†’ (𝐽 β†Ύt (-1[,]1)) = ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1)))
32298, 321ax-mp 5 . . . . 5 (𝐽 β†Ύt (-1[,]1)) = ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1))
323 ordtresticc 23047 . . . . 5 ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1)) = (ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))
324322, 323eqtri 2759 . . . 4 (𝐽 β†Ύt (-1[,]1)) = (ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))
325324oveq1i 7422 . . 3 ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ )) = ((ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))Homeo(ordTopβ€˜ ≀ ))
326318, 325eleqtrri 2831 . 2 𝐺 ∈ ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ ))
327301, 326pm3.2i 470 1 (𝐺 Isom < , < ((-1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ )))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  {cab 2708   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   ∩ 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 6539  β€“ontoβ†’wfo 6541  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   Isom wiso 6544  (class class class)co 7412  β„cr 11115  0cc0 11116  1c1 11117   + caddc 11119  +∞cpnf 11252  β„*cxr 11254   < clt 11255   ≀ cle 11256   βˆ’ cmin 11451  -cneg 11452   / cdiv 11878  -𝑒cxne 13096  [,]cicc 13334   β†Ύt crest 17373  TopOpenctopn 17374  ordTopcordt 17452  PosetRelcps 18527   TosetRel ctsr 18528  β„‚fldccnfld 21233  Homeochmeo 23577  IIcii 24715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  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 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-er 8709  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fi 9412  df-sup 9443  df-inf 9444  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-z 12566  df-dec 12685  df-uz 12830  df-q 12940  df-rp 12982  df-xneg 13099  df-xadd 13100  df-xmul 13101  df-ioo 13335  df-ioc 13336  df-ico 13337  df-icc 13338  df-fz 13492  df-seq 13974  df-exp 14035  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-struct 17087  df-slot 17122  df-ndx 17134  df-base 17152  df-plusg 17217  df-mulr 17218  df-starv 17219  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-rest 17375  df-topn 17376  df-topgen 17396  df-ordt 17454  df-ps 18529  df-tsr 18530  df-psmet 21225  df-xmet 21226  df-met 21227  df-bl 21228  df-mopn 21229  df-cnfld 21234  df-top 22716  df-topon 22733  df-topsp 22755  df-bases 22769  df-cn 23051  df-hmeo 23579  df-xms 24146  df-ms 24147  df-ii 24717
This theorem is referenced by:  xrhmph  24792
  Copyright terms: Public domain W3C validator