This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrhmeo

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

Ref Expression
Hypotheses xrhmeo.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) )
xrhmeo.g ⊢ 𝐺 = ( 𝑦 ∈ ( - 1 [,] 1 ) ↦ if ( 0 ≤ 𝑦 , ( 𝐹 ‘ 𝑦 ) , -𝑒 ( 𝐹 ‘ - 𝑦 ) ) )
xrhmeo.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion xrhmeo ( 𝐺 Isom < , < ( ( - 1 [,] 1 ) , ℝ* ) ∧ 𝐺 ∈ ( ( 𝐽 ↾t ( - 1 [,] 1 ) ) Homeo ( ordTop ‘ ≤ ) ) )

Proof

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