MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrhmeo Structured version   Visualization version   GIF version

Theorem xrhmeo 24231
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 13276 . . . 4 (-1[,]1) βŠ† ℝ*
2 xrltso 12989 . . . 4 < Or ℝ*
3 soss 5563 . . . 4 ((-1[,]1) βŠ† ℝ* β†’ ( < Or ℝ* β†’ < Or (-1[,]1)))
41, 2, 3mp2 9 . . 3 < Or (-1[,]1)
5 sopo 5562 . . . 4 ( < Or ℝ* β†’ < Po ℝ*)
62, 5ax-mp 5 . . 3 < Po ℝ*
7 xrhmeo.g . . . . 5 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8 iccssxr 13276 . . . . . . 7 (0[,]+∞) βŠ† ℝ*
9 neg1rr 12202 . . . . . . . . . . . 12 -1 ∈ ℝ
10 1re 11089 . . . . . . . . . . . 12 1 ∈ ℝ
119, 10elicc2i 13259 . . . . . . . . . . 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 13312 . . . . . . . . 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 24229 . . . . . . . . . . 11 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ ◑𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
2120simpli 485 . . . . . . . . . 10 𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞)
22 f1of 6780 . . . . . . . . . 10 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) β†’ 𝐹:(0[,]1)⟢(0[,]+∞))
2321, 22ax-mp 5 . . . . . . . . 9 𝐹:(0[,]1)⟢(0[,]+∞)
2423ffvelcdmi 7029 . . . . . . . 8 (𝑦 ∈ (0[,]1) β†’ (πΉβ€˜π‘¦) ∈ (0[,]+∞))
2518, 24syl 17 . . . . . . 7 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ (πΉβ€˜π‘¦) ∈ (0[,]+∞))
268, 25sselid 3941 . . . . . 6 ((𝑦 ∈ (-1[,]1) ∧ 0 ≀ 𝑦) β†’ (πΉβ€˜π‘¦) ∈ ℝ*)
2712adantr 482 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 𝑦 ∈ ℝ)
2827renegcld 11516 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ∈ ℝ)
29 0re 11091 . . . . . . . . . . . . 13 0 ∈ ℝ
30 letric 11189 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (0 ≀ 𝑦 ∨ 𝑦 ≀ 0))
3129, 12, 30sylancr 588 . . . . . . . . . . . 12 (𝑦 ∈ (-1[,]1) β†’ (0 ≀ 𝑦 ∨ 𝑦 ≀ 0))
3231orcanai 1002 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ 𝑦 ≀ 0)
3327le0neg1d 11660 . . . . . . . . . . 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 11593 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (-1 ≀ 𝑦 ↔ -𝑦 ≀ 1))
3810, 27, 37sylancr 588 . . . . . . . . . . 11 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (-1 ≀ 𝑦 ↔ -𝑦 ≀ 1))
3936, 38mpbid 231 . . . . . . . . . 10 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ≀ 1)
40 elicc01 13312 . . . . . . . . . 10 (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≀ -𝑦 ∧ -𝑦 ≀ 1))
4128, 34, 39, 40syl3anbrc 1344 . . . . . . . . 9 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑦 ∈ (0[,]1))
4223ffvelcdmi 7029 . . . . . . . . 9 (-𝑦 ∈ (0[,]1) β†’ (πΉβ€˜-𝑦) ∈ (0[,]+∞))
4341, 42syl 17 . . . . . . . 8 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (πΉβ€˜-𝑦) ∈ (0[,]+∞))
448, 43sselid 3941 . . . . . . 7 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ (πΉβ€˜-𝑦) ∈ ℝ*)
4544xnegcld 13148 . . . . . 6 ((𝑦 ∈ (-1[,]1) ∧ Β¬ 0 ≀ 𝑦) β†’ -𝑒(πΉβ€˜-𝑦) ∈ ℝ*)
4626, 45ifclda 4520 . . . . 5 (𝑦 ∈ (-1[,]1) β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ∈ ℝ*)
477, 46fmpti 7055 . . . 4 𝐺:(-1[,]1)βŸΆβ„*
48 frn 6671 . . . . . 6 (𝐺:(-1[,]1)βŸΆβ„* β†’ ran 𝐺 βŠ† ℝ*)
4947, 48ax-mp 5 . . . . 5 ran 𝐺 βŠ† ℝ*
50 ssabral 4018 . . . . . . 7 (ℝ* βŠ† {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))} ↔ βˆ€π‘§ ∈ ℝ* βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
51 0le1 11612 . . . . . . . . . . . . 13 0 ≀ 1
52 le0neg2 11598 . . . . . . . . . . . . . 14 (1 ∈ ℝ β†’ (0 ≀ 1 ↔ -1 ≀ 0))
5310, 52ax-mp 5 . . . . . . . . . . . . 13 (0 ≀ 1 ↔ -1 ≀ 0)
5451, 53mpbi 229 . . . . . . . . . . . 12 -1 ≀ 0
55 1le1 11717 . . . . . . . . . . . 12 1 ≀ 1
56 iccss 13261 . . . . . . . . . . . 12 (((-1 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (-1 ≀ 0 ∧ 1 ≀ 1)) β†’ (0[,]1) βŠ† (-1[,]1))
579, 10, 54, 55, 56mp4an 692 . . . . . . . . . . 11 (0[,]1) βŠ† (-1[,]1)
58 elxrge0 13303 . . . . . . . . . . . 12 (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧))
59 f1ocnv 6792 . . . . . . . . . . . . . 14 (𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) β†’ ◑𝐹:(0[,]+∞)–1-1-ontoβ†’(0[,]1))
60 f1of 6780 . . . . . . . . . . . . . 14 (◑𝐹:(0[,]+∞)–1-1-ontoβ†’(0[,]1) β†’ ◑𝐹:(0[,]+∞)⟢(0[,]1))
6121, 59, 60mp2b 10 . . . . . . . . . . . . 13 ◑𝐹:(0[,]+∞)⟢(0[,]1)
6261ffvelcdmi 7029 . . . . . . . . . . . 12 (𝑧 ∈ (0[,]+∞) β†’ (β—‘πΉβ€˜π‘§) ∈ (0[,]1))
6358, 62sylbir 234 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜π‘§) ∈ (0[,]1))
6457, 63sselid 3941 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜π‘§) ∈ (-1[,]1))
65 elicc01 13312 . . . . . . . . . . . 12 ((β—‘πΉβ€˜π‘§) ∈ (0[,]1) ↔ ((β—‘πΉβ€˜π‘§) ∈ ℝ ∧ 0 ≀ (β—‘πΉβ€˜π‘§) ∧ (β—‘πΉβ€˜π‘§) ≀ 1))
6665simp2bi 1147 . . . . . . . . . . 11 ((β—‘πΉβ€˜π‘§) ∈ (0[,]1) β†’ 0 ≀ (β—‘πΉβ€˜π‘§))
6763, 66syl 17 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 0 ≀ (β—‘πΉβ€˜π‘§))
6858biimpri 227 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ (0[,]+∞))
69 f1ocnvfv2 7218 . . . . . . . . . . . 12 ((𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘§)) = 𝑧)
7021, 68, 69sylancr 588 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘§)) = 𝑧)
7170eqcomd 2744 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))
72 breq2 5108 . . . . . . . . . . . 12 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (0 ≀ 𝑦 ↔ 0 ≀ (β—‘πΉβ€˜π‘§)))
73 fveq2 6838 . . . . . . . . . . . . 13 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜(β—‘πΉβ€˜π‘§)))
7473eqeq2d 2749 . . . . . . . . . . . 12 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ (𝑧 = (πΉβ€˜π‘¦) ↔ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§))))
7572, 74anbi12d 632 . . . . . . . . . . 11 (𝑦 = (β—‘πΉβ€˜π‘§) β†’ ((0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) ↔ (0 ≀ (β—‘πΉβ€˜π‘§) ∧ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))))
7675rspcev 3580 . . . . . . . . . 10 (((β—‘πΉβ€˜π‘§) ∈ (-1[,]1) ∧ (0 ≀ (β—‘πΉβ€˜π‘§) ∧ 𝑧 = (πΉβ€˜(β—‘πΉβ€˜π‘§)))) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)))
7764, 67, 71, 76syl12anc 836 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)))
78 iftrue 4491 . . . . . . . . . . . 12 (0 ≀ 𝑦 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = (πΉβ€˜π‘¦))
7978eqeq2d 2749 . . . . . . . . . . 11 (0 ≀ 𝑦 β†’ (𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ↔ 𝑧 = (πΉβ€˜π‘¦)))
8079biimpar 479 . . . . . . . . . 10 ((0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) β†’ 𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8180reximi 3086 . . . . . . . . 9 (βˆƒπ‘¦ ∈ (-1[,]1)(0 ≀ 𝑦 ∧ 𝑧 = (πΉβ€˜π‘¦)) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
8277, 81syl 17 . . . . . . . 8 ((𝑧 ∈ ℝ* ∧ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
83 xnegcl 13061 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℝ* β†’ -𝑒𝑧 ∈ ℝ*)
8483adantr 482 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒𝑧 ∈ ℝ*)
85 0xr 11136 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ*
86 xrletri 13001 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) β†’ (0 ≀ 𝑧 ∨ 𝑧 ≀ 0))
8785, 86mpan 689 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℝ* β†’ (0 ≀ 𝑧 ∨ 𝑧 ≀ 0))
8887ord 863 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 β†’ 𝑧 ≀ 0))
89 xle0neg1 13069 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℝ* β†’ (𝑧 ≀ 0 ↔ 0 ≀ -𝑒𝑧))
9088, 89sylibd 238 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 β†’ 0 ≀ -𝑒𝑧))
9190imp 408 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ 0 ≀ -𝑒𝑧)
92 elxrge0 13303 . . . . . . . . . . . . . . 15 (-𝑒𝑧 ∈ (0[,]+∞) ↔ (-𝑒𝑧 ∈ ℝ* ∧ 0 ≀ -𝑒𝑧))
9384, 91, 92sylanbrc 584 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒𝑧 ∈ (0[,]+∞))
9461ffvelcdmi 7029 . . . . . . . . . . . . . 14 (-𝑒𝑧 ∈ (0[,]+∞) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1))
9593, 94syl 17 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (0[,]1))
9657, 95sselid 3941 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1))
97 iccssre 13275 . . . . . . . . . . . . . . 15 ((-1 ∈ ℝ ∧ 1 ∈ ℝ) β†’ (-1[,]1) βŠ† ℝ)
989, 10, 97mp2an 691 . . . . . . . . . . . . . 14 (-1[,]1) βŠ† ℝ
9998, 96sselid 3941 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ)
100 iccneg 13318 . . . . . . . . . . . . . 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 12205 . . . . . . . . . . . 12 --1 = 1
105104oveq2i 7361 . . . . . . . . . . 11 (-1[,]--1) = (-1[,]1)
106103, 105eleqtrdi 2849 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1))
107 xle0neg2 13070 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℝ* β†’ (0 ≀ 𝑧 ↔ -𝑒𝑧 ≀ 0))
108107notbid 318 . . . . . . . . . . . . . 14 (𝑧 ∈ ℝ* β†’ (Β¬ 0 ≀ 𝑧 ↔ Β¬ -𝑒𝑧 ≀ 0))
109108biimpa 478 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ -𝑒𝑧 ≀ 0)
110 f1ocnvfv2 7218 . . . . . . . . . . . . . . 15 ((𝐹:(0[,]1)–1-1-ontoβ†’(0[,]+∞) ∧ -𝑒𝑧 ∈ (0[,]+∞)) β†’ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
11121, 93, 110sylancr 588 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
112 0elunit 13315 . . . . . . . . . . . . . . . 16 0 ∈ (0[,]1)
113 ax-1ne0 11054 . . . . . . . . . . . . . . . . . . . . 21 1 β‰  0
114 neeq2 3006 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 0 β†’ (1 β‰  π‘₯ ↔ 1 β‰  0))
115113, 114mpbiri 258 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ 1 β‰  π‘₯)
116115necomd 2998 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 0 β†’ π‘₯ β‰  1)
117 ifnefalse 4497 . . . . . . . . . . . . . . . . . . 19 (π‘₯ β‰  1 β†’ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))) = (π‘₯ / (1 βˆ’ π‘₯)))
118116, 117syl 17 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 0 β†’ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))) = (π‘₯ / (1 βˆ’ π‘₯)))
119 id 22 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ π‘₯ = 0)
120 oveq2 7358 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 0 β†’ (1 βˆ’ π‘₯) = (1 βˆ’ 0))
121 1m0e1 12208 . . . . . . . . . . . . . . . . . . . . 21 (1 βˆ’ 0) = 1
122120, 121eqtrdi 2794 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 0 β†’ (1 βˆ’ π‘₯) = 1)
123119, 122oveq12d 7368 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 0 β†’ (π‘₯ / (1 βˆ’ π‘₯)) = (0 / 1))
124 ax-1cn 11043 . . . . . . . . . . . . . . . . . . . 20 1 ∈ β„‚
125124, 113div0i 11823 . . . . . . . . . . . . . . . . . . 19 (0 / 1) = 0
126123, 125eqtrdi 2794 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 0 β†’ (π‘₯ / (1 βˆ’ π‘₯)) = 0)
127118, 126eqtrd 2778 . . . . . . . . . . . . . . . . 17 (π‘₯ = 0 β†’ if(π‘₯ = 1, +∞, (π‘₯ / (1 βˆ’ π‘₯))) = 0)
128 c0ex 11083 . . . . . . . . . . . . . . . . 17 0 ∈ V
129127, 19, 128fvmpt 6944 . . . . . . . . . . . . . . . 16 (0 ∈ (0[,]1) β†’ (πΉβ€˜0) = 0)
130112, 129ax-mp 5 . . . . . . . . . . . . . . 15 (πΉβ€˜0) = 0
131130a1i 11 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜0) = 0)
132111, 131breq12d 5117 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0) ↔ -𝑒𝑧 ≀ 0))
133109, 132mtbird 325 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)) ≀ (πΉβ€˜0))
134 eqid 2738 . . . . . . . . . . . . . . . 16 ((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞)) = ((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞))
13519, 134iccpnfhmeo 24230 . . . . . . . . . . . . . . 15 (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTopβ€˜ ≀ ) β†Ύt (0[,]+∞))))
136135simpli 485 . . . . . . . . . . . . . 14 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137 iccssxr 13276 . . . . . . . . . . . . . . 15 (0[,]1) βŠ† ℝ*
138137, 8pm3.2i 472 . . . . . . . . . . . . . 14 ((0[,]1) βŠ† ℝ* ∧ (0[,]+∞) βŠ† ℝ*)
139 leisorel 14287 . . . . . . . . . . . . . 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 11660 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ ((β—‘πΉβ€˜-𝑒𝑧) ≀ 0 ↔ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
144142, 143mtbid 324 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧))
145 unitssre 13345 . . . . . . . . . . . . . . . . 17 (0[,]1) βŠ† ℝ
146145, 95sselid 3941 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ ℝ)
147146recnd 11117 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (β—‘πΉβ€˜-𝑒𝑧) ∈ β„‚)
148147negnegd 11437 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ --(β—‘πΉβ€˜-𝑒𝑧) = (β—‘πΉβ€˜-𝑒𝑧))
149148fveq2d 6842 . . . . . . . . . . . . 13 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = (πΉβ€˜(β—‘πΉβ€˜-𝑒𝑧)))
150149, 111eqtrd 2778 . . . . . . . . . . . 12 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧)
151 xnegeq 13055 . . . . . . . . . . . 12 ((πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒𝑧 β†’ -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒-𝑒𝑧)
152150, 151syl 17 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) = -𝑒-𝑒𝑧)
153 xnegneg 13062 . . . . . . . . . . . 12 (𝑧 ∈ ℝ* β†’ -𝑒-𝑒𝑧 = 𝑧)
154153adantr 482 . . . . . . . . . . 11 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒-𝑒𝑧 = 𝑧)
155152, 154eqtr2d 2779 . . . . . . . . . 10 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
156 breq2 5108 . . . . . . . . . . . . 13 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (0 ≀ 𝑦 ↔ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
157156notbid 318 . . . . . . . . . . . 12 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (Β¬ 0 ≀ 𝑦 ↔ Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧)))
158 negeq 11327 . . . . . . . . . . . . . . 15 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ -𝑦 = --(β—‘πΉβ€˜-𝑒𝑧))
159158fveq2d 6842 . . . . . . . . . . . . . 14 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (πΉβ€˜-𝑦) = (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
160 xnegeq 13055 . . . . . . . . . . . . . 14 ((πΉβ€˜-𝑦) = (πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
161159, 160syl 17 . . . . . . . . . . . . 13 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))
162161eqeq2d 2749 . . . . . . . . . . . 12 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ (𝑧 = -𝑒(πΉβ€˜-𝑦) ↔ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧))))
163157, 162anbi12d 632 . . . . . . . . . . 11 (𝑦 = -(β—‘πΉβ€˜-𝑒𝑧) β†’ ((Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) ↔ (Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧) ∧ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))))
164163rspcev 3580 . . . . . . . . . 10 ((-(β—‘πΉβ€˜-𝑒𝑧) ∈ (-1[,]1) ∧ (Β¬ 0 ≀ -(β—‘πΉβ€˜-𝑒𝑧) ∧ 𝑧 = -𝑒(πΉβ€˜--(β—‘πΉβ€˜-𝑒𝑧)))) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
165106, 144, 155, 164syl12anc 836 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ Β¬ 0 ≀ 𝑧) β†’ βˆƒπ‘¦ ∈ (-1[,]1)(Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
166 iffalse 4494 . . . . . . . . . . . 12 (Β¬ 0 ≀ 𝑦 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = -𝑒(πΉβ€˜-𝑦))
167166eqeq2d 2749 . . . . . . . . . . 11 (Β¬ 0 ≀ 𝑦 β†’ (𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) ↔ 𝑧 = -𝑒(πΉβ€˜-𝑦)))
168167biimpar 479 . . . . . . . . . 10 ((Β¬ 0 ≀ 𝑦 ∧ 𝑧 = -𝑒(πΉβ€˜-𝑦)) β†’ 𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)))
169168reximi 3086 . . . . . . . . 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 3070 . . . . . 6 ℝ* βŠ† {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))}
1737rnmpt 5907 . . . . . 6 ran 𝐺 = {𝑧 ∣ βˆƒπ‘¦ ∈ (-1[,]1)𝑧 = if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦))}
174172, 173sseqtrri 3980 . . . . 5 ℝ* βŠ† ran 𝐺
17549, 174eqssi 3959 . . . 4 ran 𝐺 = ℝ*
176 dffo2 6756 . . . 4 (𝐺:(-1[,]1)–onto→ℝ* ↔ (𝐺:(-1[,]1)βŸΆβ„* ∧ ran 𝐺 = ℝ*))
17747, 175, 176mpbir2an 710 . . 3 𝐺:(-1[,]1)–onto→ℝ*
178 breq1 5107 . . . . . . 7 ((πΉβ€˜π‘§) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) β†’ ((πΉβ€˜π‘§) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) ↔ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
179 breq1 5107 . . . . . . 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 5108 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ (0 ≀ 𝑦 ↔ 0 ≀ 𝑧))
184 eleq1w 2821 . . . . . . . . . . . . 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 3533 . . . . . . . . . . 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 3941 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ∈ ℝ)
19298, 189sselid 3941 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑀 ∈ ℝ)
193191, 192, 180ltled 11237 . . . . . . . . . . . 12 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑧 ≀ 𝑀)
194190, 191, 192, 182, 193letrd 11246 . . . . . . . . . . 11 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 0 ≀ 𝑀)
195 breq2 5108 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ (0 ≀ 𝑦 ↔ 0 ≀ 𝑀))
196 eleq1w 2821 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ (𝑦 ∈ (0[,]1) ↔ 𝑀 ∈ (0[,]1)))
197195, 196imbi12d 345 . . . . . . . . . . . 12 (𝑦 = 𝑀 β†’ ((0 ≀ 𝑦 β†’ 𝑦 ∈ (0[,]1)) ↔ (0 ≀ 𝑀 β†’ 𝑀 ∈ (0[,]1))))
198197, 186vtoclga 3533 . . . . . . . . . . 11 (𝑀 ∈ (-1[,]1) β†’ (0 ≀ 𝑀 β†’ 𝑀 ∈ (0[,]1)))
199189, 194, 198sylc 65 . . . . . . . . . 10 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ 𝑀 ∈ (0[,]1))
200 isorel 7266 . . . . . . . . . . 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 4493 . . . . . . . 8 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) = (πΉβ€˜π‘€))
205203, 204breqtrrd 5132 . . . . . . 7 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ 0 ≀ 𝑧) β†’ (πΉβ€˜π‘§) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
206 breq2 5108 . . . . . . . 8 ((πΉβ€˜π‘€) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) β†’ (-𝑒(πΉβ€˜-𝑧) < (πΉβ€˜π‘€) ↔ -𝑒(πΉβ€˜-𝑧) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
207 breq2 5108 . . . . . . . 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 11327 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 β†’ -𝑦 = -𝑧)
212211eleq1d 2823 . . . . . . . . . . . . . . . 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 3533 . . . . . . . . . . . . . 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 7029 . . . . . . . . . . . 12 (-𝑧 ∈ (0[,]1) β†’ (πΉβ€˜-𝑧) ∈ (0[,]+∞))
219217, 218syl 17 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ (0[,]+∞))
2208, 219sselid 3941 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ ℝ*)
221220xnegcld 13148 . . . . . . . . 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 7029 . . . . . . . . . . 11 (𝑀 ∈ (0[,]1) β†’ (πΉβ€˜π‘€) ∈ (0[,]+∞))
227225, 226syl 17 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (πΉβ€˜π‘€) ∈ (0[,]+∞))
2288, 227sselid 3941 . . . . . . . . 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 3941 . . . . . . . . . . . . . . 15 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 𝑧 ∈ ℝ)
232 ltnle 11168 . . . . . . . . . . . . . . 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 11658 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ (𝑧 < 0 ↔ 0 < -𝑧))
236234, 235mpbid 231 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 < -𝑧)
237 isorel 7266 . . . . . . . . . . . . . 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 5140 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 < (πΉβ€˜-𝑧))
242 xlt0neg2 13068 . . . . . . . . . . 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 13303 . . . . . . . . . . 11 ((πΉβ€˜π‘€) ∈ (0[,]+∞) ↔ ((πΉβ€˜π‘€) ∈ ℝ* ∧ 0 ≀ (πΉβ€˜π‘€)))
246245simprbi 498 . . . . . . . . . 10 ((πΉβ€˜π‘€) ∈ (0[,]+∞) β†’ 0 ≀ (πΉβ€˜π‘€))
247227, 246syl 17 . . . . . . . . 9 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ 0 ≀ 𝑀) β†’ 0 ≀ (πΉβ€˜π‘€))
248221, 222, 228, 244, 247xrltletrd 13009 . . . . . . . 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 3941 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑧 ∈ ℝ)
252 simpll2 1214 . . . . . . . . . . . . 13 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑀 ∈ (-1[,]1))
25398, 252sselid 3941 . . . . . . . . . . . 12 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ 𝑀 ∈ ℝ)
254251, 253ltnegd 11667 . . . . . . . . . . 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 11327 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 β†’ -𝑦 = -𝑀)
259258eleq1d 2823 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 β†’ (-𝑦 ∈ (0[,]1) ↔ -𝑀 ∈ (0[,]1)))
260257, 259imbi12d 345 . . . . . . . . . . . . 13 (𝑦 = 𝑀 β†’ ((Β¬ 0 ≀ 𝑦 β†’ -𝑦 ∈ (0[,]1)) ↔ (Β¬ 0 ≀ 𝑀 β†’ -𝑀 ∈ (0[,]1))))
261260, 214vtoclga 3533 . . . . . . . . . . . 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 7266 . . . . . . . . . . . 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 7029 . . . . . . . . . . . 12 (-𝑀 ∈ (0[,]1) β†’ (πΉβ€˜-𝑀) ∈ (0[,]+∞))
269262, 268syl 17 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑀) ∈ (0[,]+∞))
2708, 269sselid 3941 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑀) ∈ ℝ*)
271263, 218syl 17 . . . . . . . . . . 11 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ (0[,]+∞))
2728, 271sselid 3941 . . . . . . . . . 10 ((((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) ∧ Β¬ 0 ≀ 𝑀) β†’ (πΉβ€˜-𝑧) ∈ ℝ*)
273 xltneg 13065 . . . . . . . . . 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 4523 . . . . . . 7 (((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) ∧ Β¬ 0 ≀ 𝑧) β†’ -𝑒(πΉβ€˜-𝑧) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
277178, 179, 205, 276ifbothda 4523 . . . . . 6 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1) ∧ 𝑧 < 𝑀) β†’ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
2782773expia 1122 . . . . 5 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1)) β†’ (𝑧 < 𝑀 β†’ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
279 fveq2 6838 . . . . . . . 8 (𝑦 = 𝑧 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘§))
280211fveq2d 6842 . . . . . . . . 9 (𝑦 = 𝑧 β†’ (πΉβ€˜-𝑦) = (πΉβ€˜-𝑧))
281 xnegeq 13055 . . . . . . . . 9 ((πΉβ€˜-𝑦) = (πΉβ€˜-𝑧) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑧))
282280, 281syl 17 . . . . . . . 8 (𝑦 = 𝑧 β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑧))
283183, 279, 282ifbieq12d 4513 . . . . . . 7 (𝑦 = 𝑧 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)))
284 fvex 6851 . . . . . . . 8 (πΉβ€˜π‘§) ∈ V
285 xnegex 13056 . . . . . . . 8 -𝑒(πΉβ€˜-𝑧) ∈ V
286284, 285ifex 4535 . . . . . . 7 if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) ∈ V
287283, 7, 286fvmpt 6944 . . . . . 6 (𝑧 ∈ (-1[,]1) β†’ (πΊβ€˜π‘§) = if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)))
288 fveq2 6838 . . . . . . . 8 (𝑦 = 𝑀 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘€))
289258fveq2d 6842 . . . . . . . . 9 (𝑦 = 𝑀 β†’ (πΉβ€˜-𝑦) = (πΉβ€˜-𝑀))
290 xnegeq 13055 . . . . . . . . 9 ((πΉβ€˜-𝑦) = (πΉβ€˜-𝑀) β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑀))
291289, 290syl 17 . . . . . . . 8 (𝑦 = 𝑀 β†’ -𝑒(πΉβ€˜-𝑦) = -𝑒(πΉβ€˜-𝑀))
292195, 288, 291ifbieq12d 4513 . . . . . . 7 (𝑦 = 𝑀 β†’ if(0 ≀ 𝑦, (πΉβ€˜π‘¦), -𝑒(πΉβ€˜-𝑦)) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
293 fvex 6851 . . . . . . . 8 (πΉβ€˜π‘€) ∈ V
294 xnegex 13056 . . . . . . . 8 -𝑒(πΉβ€˜-𝑀) ∈ V
295293, 294ifex 4535 . . . . . . 7 if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)) ∈ V
296292, 7, 295fvmpt 6944 . . . . . 6 (𝑀 ∈ (-1[,]1) β†’ (πΊβ€˜π‘€) = if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀)))
297287, 296breqan12d 5120 . . . . 5 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1)) β†’ ((πΊβ€˜π‘§) < (πΊβ€˜π‘€) ↔ if(0 ≀ 𝑧, (πΉβ€˜π‘§), -𝑒(πΉβ€˜-𝑧)) < if(0 ≀ 𝑀, (πΉβ€˜π‘€), -𝑒(πΉβ€˜-𝑀))))
298278, 297sylibrd 259 . . . 4 ((𝑧 ∈ (-1[,]1) ∧ 𝑀 ∈ (-1[,]1)) β†’ (𝑧 < 𝑀 β†’ (πΊβ€˜π‘§) < (πΊβ€˜π‘€)))
299298rgen2 3193 . . 3 βˆ€π‘§ ∈ (-1[,]1)βˆ€π‘€ ∈ (-1[,]1)(𝑧 < 𝑀 β†’ (πΊβ€˜π‘§) < (πΊβ€˜π‘€))
300 soisoi 7268 . . 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 18417 . . . . . 6 ≀ ∈ TosetRel
303302elexi 3463 . . . . 5 ≀ ∈ V
304303inex1 5273 . . . 4 ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) ∈ V
305 ssid 3965 . . . . . . 7 ℝ* βŠ† ℝ*
306 leiso 14286 . . . . . . 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 7274 . . . . 5 (𝐺 Isom ≀ , ≀ ((-1[,]1), ℝ*) ↔ 𝐺 Isom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))), ≀ ((-1[,]1), ℝ*))
310308, 309mpbi 229 . . . 4 𝐺 Isom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))), ≀ ((-1[,]1), ℝ*)
311 tsrps 18411 . . . . . . . 8 ( ≀ ∈ TosetRel β†’ ≀ ∈ PosetRel)
312302, 311ax-mp 5 . . . . . . 7 ≀ ∈ PosetRel
313 ledm 18414 . . . . . . . 8 ℝ* = dom ≀
314313psssdm 18406 . . . . . . 7 (( ≀ ∈ PosetRel ∧ (-1[,]1) βŠ† ℝ*) β†’ dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) = (-1[,]1))
315312, 1, 314mp2an 691 . . . . . 6 dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))) = (-1[,]1)
316315eqcomi 2747 . . . . 5 (-1[,]1) = dom ( ≀ ∩ ((-1[,]1) Γ— (-1[,]1)))
317316, 313ordthmeo 23075 . . . 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 2738 . . . . . . 7 (ordTopβ€˜ ≀ ) = (ordTopβ€˜ ≀ )
321319, 320xrrest2 24093 . . . . . 6 ((-1[,]1) βŠ† ℝ β†’ (𝐽 β†Ύt (-1[,]1)) = ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1)))
32298, 321ax-mp 5 . . . . 5 (𝐽 β†Ύt (-1[,]1)) = ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1))
323 ordtresticc 22496 . . . . 5 ((ordTopβ€˜ ≀ ) β†Ύt (-1[,]1)) = (ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))
324322, 323eqtri 2766 . . . 4 (𝐽 β†Ύt (-1[,]1)) = (ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))
325324oveq1i 7360 . . 3 ((𝐽 β†Ύt (-1[,]1))Homeo(ordTopβ€˜ ≀ )) = ((ordTopβ€˜( ≀ ∩ ((-1[,]1) Γ— (-1[,]1))))Homeo(ordTopβ€˜ ≀ ))
326318, 325eleqtrri 2838 . 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 2715   β‰  wne 2942  βˆ€wral 3063  βˆƒwrex 3072  Vcvv 3444   ∩ cin 3908   βŠ† wss 3909  ifcif 4485   class class class wbr 5104   ↦ cmpt 5187   Po wpo 5541   Or wor 5542   Γ— cxp 5629  β—‘ccnv 5630  dom cdm 5631  ran crn 5632  βŸΆwf 6488  β€“ontoβ†’wfo 6490  β€“1-1-ontoβ†’wf1o 6491  β€˜cfv 6492   Isom wiso 6493  (class class class)co 7350  β„cr 10984  0cc0 10985  1c1 10986   + caddc 10988  +∞cpnf 11120  β„*cxr 11122   < clt 11123   ≀ cle 11124   βˆ’ cmin 11319  -cneg 11320   / cdiv 11746  -𝑒cxne 12959  [,]cicc 13196   β†Ύt crest 17237  TopOpenctopn 17238  ordTopcordt 17316  PosetRelcps 18388   TosetRel ctsr 18389  β„‚fldccnfld 20719  Homeochmeo 23026  IIcii 24160
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 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063
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 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-iin 4956  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-er 8582  df-map 8701  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fi 9281  df-sup 9312  df-inf 9313  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-5 12153  df-6 12154  df-7 12155  df-8 12156  df-9 12157  df-n0 12348  df-z 12434  df-dec 12552  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ioc 13198  df-ico 13199  df-icc 13200  df-fz 13354  df-seq 13836  df-exp 13897  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-struct 16954  df-slot 16989  df-ndx 17001  df-base 17019  df-plusg 17081  df-mulr 17082  df-starv 17083  df-tset 17087  df-ple 17088  df-ds 17090  df-unif 17091  df-rest 17239  df-topn 17240  df-topgen 17260  df-ordt 17318  df-ps 18390  df-tsr 18391  df-psmet 20711  df-xmet 20712  df-met 20713  df-bl 20714  df-mopn 20715  df-cnfld 20720  df-top 22165  df-topon 22182  df-topsp 22204  df-bases 22218  df-cn 22500  df-hmeo 23028  df-xms 23595  df-ms 23596  df-ii 24162
This theorem is referenced by:  xrhmph  24232
  Copyright terms: Public domain W3C validator