Metamath Proof Explorer

Theorem xrge0iifiso

Description: The defined bijection from the closed unit interval onto the extended nonnegative reals is an order isomorphism. (Contributed by Thierry Arnoux, 31-Mar-2017)

Ref Expression
Hypothesis xrge0iifhmeo.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
Assertion xrge0iifiso 𝐹 Isom < , ◡ < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
2 iccssxr ⊢ ( 0 [,] 1 ) ⊆ ℝ*
3 xrltso ⊢ < Or ℝ*
4 soss ⊢ ( ( 0 [,] 1 ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] 1 ) ) )
5 2 3 4 mp2 ⊢ < Or ( 0 [,] 1 )
6 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
7 cnvso ⊢ ( < Or ℝ* ↔ ◡ < Or ℝ* )
8 3 7 mpbi ⊢ ◡ < Or ℝ*
9 sopo ⊢ ( ◡ < Or ℝ* → ◡ < Po ℝ* )
10 8 9 ax-mp ⊢ ◡ < Po ℝ*
11 poss ⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( ◡ < Po ℝ* → ◡ < Po ( 0 [,] +∞ ) ) )
12 6 10 11 mp2 ⊢ ◡ < Po ( 0 [,] +∞ )
13 1 xrge0iifcnv ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑧 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑧 = +∞ , 0 , ( exp ‘ - 𝑧 ) ) ) )
14 13 simpli ⊢ 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ )
15 f1ofo ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) → 𝐹 : ( 0 [,] 1 ) –onto→ ( 0 [,] +∞ ) )
16 14 15 ax-mp ⊢ 𝐹 : ( 0 [,] 1 ) –onto→ ( 0 [,] +∞ )
17 0xr ⊢ 0 ∈ ℝ*
18 1xr ⊢ 1 ∈ ℝ*
19 0le1 ⊢ 0 ≤ 1
20 snunioc ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1 ) → ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 ) )
21 17 18 19 20 mp3an ⊢ ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 )
22 21 eleq2i ⊢ ( 𝑤 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ↔ 𝑤 ∈ ( 0 [,] 1 ) )
23 elun ⊢ ( 𝑤 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ↔ ( 𝑤 ∈ { 0 } ∨ 𝑤 ∈ ( 0 (,] 1 ) ) )
24 22 23 bitr3i ⊢ ( 𝑤 ∈ ( 0 [,] 1 ) ↔ ( 𝑤 ∈ { 0 } ∨ 𝑤 ∈ ( 0 (,] 1 ) ) )
25 velsn ⊢ ( 𝑤 ∈ { 0 } ↔ 𝑤 = 0 )
26 elunitrn ⊢ ( 𝑧 ∈ ( 0 [,] 1 ) → 𝑧 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 0 < 𝑧 ) → 𝑧 ∈ ℝ )
28 simpr ⊢ ( ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 0 < 𝑧 ) → 0 < 𝑧 )
29 elicc01 ⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 ≤ 𝑧 ∧ 𝑧 ≤ 1 ) )
30 29 simp3bi ⊢ ( 𝑧 ∈ ( 0 [,] 1 ) → 𝑧 ≤ 1 )
31 30 adantr ⊢ ( ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 0 < 𝑧 ) → 𝑧 ≤ 1 )
32 1re ⊢ 1 ∈ ℝ
33 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝑧 ∈ ( 0 (,] 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ∧ 𝑧 ≤ 1 ) ) )
34 17 32 33 mp2an ⊢ ( 𝑧 ∈ ( 0 (,] 1 ) ↔ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ∧ 𝑧 ≤ 1 ) )
35 27 28 31 34 syl3anbrc ⊢ ( ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 0 < 𝑧 ) → 𝑧 ∈ ( 0 (,] 1 ) )
36 pnfxr ⊢ +∞ ∈ ℝ*
37 0le0 ⊢ 0 ≤ 0
38 ltpnf ⊢ ( 1 ∈ ℝ → 1 < +∞ )
39 32 38 ax-mp ⊢ 1 < +∞
40 iocssioo ⊢ ( ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ 1 < +∞ ) ) → ( 0 (,] 1 ) ⊆ ( 0 (,) +∞ ) )
41 17 36 37 39 40 mp4an ⊢ ( 0 (,] 1 ) ⊆ ( 0 (,) +∞ )
42 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
43 41 42 sseqtri ⊢ ( 0 (,] 1 ) ⊆ ℝ+
44 43 sseli ⊢ ( 𝑧 ∈ ( 0 (,] 1 ) → 𝑧 ∈ ℝ+ )
45 relogcl ⊢ ( 𝑧 ∈ ℝ+ → ( log ‘ 𝑧 ) ∈ ℝ )
46 45 renegcld ⊢ ( 𝑧 ∈ ℝ+ → - ( log ‘ 𝑧 ) ∈ ℝ )
47 ltpnf ⊢ ( - ( log ‘ 𝑧 ) ∈ ℝ → - ( log ‘ 𝑧 ) < +∞ )
48 46 47 syl ⊢ ( 𝑧 ∈ ℝ+ → - ( log ‘ 𝑧 ) < +∞ )
49 brcnvg ⊢ ( ( +∞ ∈ ℝ* ∧ - ( log ‘ 𝑧 ) ∈ ℝ ) → ( +∞ ◡ < - ( log ‘ 𝑧 ) ↔ - ( log ‘ 𝑧 ) < +∞ ) )
50 36 46 49 sylancr ⊢ ( 𝑧 ∈ ℝ+ → ( +∞ ◡ < - ( log ‘ 𝑧 ) ↔ - ( log ‘ 𝑧 ) < +∞ ) )
51 48 50 mpbird ⊢ ( 𝑧 ∈ ℝ+ → +∞ ◡ < - ( log ‘ 𝑧 ) )
52 44 51 syl ⊢ ( 𝑧 ∈ ( 0 (,] 1 ) → +∞ ◡ < - ( log ‘ 𝑧 ) )
53 1 xrge0iifcv ⊢ ( 𝑧 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑧 ) = - ( log ‘ 𝑧 ) )
54 52 53 breqtrrd ⊢ ( 𝑧 ∈ ( 0 (,] 1 ) → +∞ ◡ < ( 𝐹 ‘ 𝑧 ) )
55 35 54 syl ⊢ ( ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 0 < 𝑧 ) → +∞ ◡ < ( 𝐹 ‘ 𝑧 ) )
56 55 ex ⊢ ( 𝑧 ∈ ( 0 [,] 1 ) → ( 0 < 𝑧 → +∞ ◡ < ( 𝐹 ‘ 𝑧 ) ) )
57 breq1 ⊢ ( 𝑤 = 0 → ( 𝑤 < 𝑧 ↔ 0 < 𝑧 ) )
58 fveq2 ⊢ ( 𝑤 = 0 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 0 ) )
59 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
60 iftrue ⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = +∞ )
61 pnfex ⊢ +∞ ∈ V
62 60 1 61 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 0 ) = +∞ )
63 59 62 ax-mp ⊢ ( 𝐹 ‘ 0 ) = +∞
64 58 63 eqtrdi ⊢ ( 𝑤 = 0 → ( 𝐹 ‘ 𝑤 ) = +∞ )
65 64 breq1d ⊢ ( 𝑤 = 0 → ( ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ↔ +∞ ◡ < ( 𝐹 ‘ 𝑧 ) ) )
66 57 65 imbi12d ⊢ ( 𝑤 = 0 → ( ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) ↔ ( 0 < 𝑧 → +∞ ◡ < ( 𝐹 ‘ 𝑧 ) ) ) )
67 56 66 imbitrrid ⊢ ( 𝑤 = 0 → ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) ) )
68 25 67 sylbi ⊢ ( 𝑤 ∈ { 0 } → ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) ) )
69 simpll ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 𝑤 ∈ ( 0 (,] 1 ) )
70 26 ad2antlr ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 𝑧 ∈ ℝ )
71 0re ⊢ 0 ∈ ℝ
72 71 a1i ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 0 ∈ ℝ )
73 43 sseli ⊢ ( 𝑤 ∈ ( 0 (,] 1 ) → 𝑤 ∈ ℝ+ )
74 73 rpred ⊢ ( 𝑤 ∈ ( 0 (,] 1 ) → 𝑤 ∈ ℝ )
75 74 ad2antrr ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 𝑤 ∈ ℝ )
76 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝑤 ∈ ( 0 (,] 1 ) ↔ ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ∧ 𝑤 ≤ 1 ) ) )
77 17 32 76 mp2an ⊢ ( 𝑤 ∈ ( 0 (,] 1 ) ↔ ( 𝑤 ∈ ℝ ∧ 0 < 𝑤 ∧ 𝑤 ≤ 1 ) )
78 77 simp2bi ⊢ ( 𝑤 ∈ ( 0 (,] 1 ) → 0 < 𝑤 )
79 78 ad2antrr ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 0 < 𝑤 )
80 simpr ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 𝑤 < 𝑧 )
81 72 75 70 79 80 lttrd ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 0 < 𝑧 )
82 30 ad2antlr ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 𝑧 ≤ 1 )
83 70 81 82 34 syl3anbrc ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → 𝑧 ∈ ( 0 (,] 1 ) )
84 69 83 jca ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) )
85 73 adantr ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → 𝑤 ∈ ℝ+ )
86 85 relogcld ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( log ‘ 𝑤 ) ∈ ℝ )
87 44 adantl ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → 𝑧 ∈ ℝ+ )
88 87 relogcld ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( log ‘ 𝑧 ) ∈ ℝ )
89 86 88 ltnegd ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( ( log ‘ 𝑤 ) < ( log ‘ 𝑧 ) ↔ - ( log ‘ 𝑧 ) < - ( log ‘ 𝑤 ) ) )
90 logltb ⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → ( 𝑤 < 𝑧 ↔ ( log ‘ 𝑤 ) < ( log ‘ 𝑧 ) ) )
91 73 44 90 syl2an ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( 𝑤 < 𝑧 ↔ ( log ‘ 𝑤 ) < ( log ‘ 𝑧 ) ) )
92 negex ⊢ - ( log ‘ 𝑤 ) ∈ V
93 negex ⊢ - ( log ‘ 𝑧 ) ∈ V
94 92 93 brcnv ⊢ ( - ( log ‘ 𝑤 ) ◡ < - ( log ‘ 𝑧 ) ↔ - ( log ‘ 𝑧 ) < - ( log ‘ 𝑤 ) )
95 94 a1i ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( - ( log ‘ 𝑤 ) ◡ < - ( log ‘ 𝑧 ) ↔ - ( log ‘ 𝑧 ) < - ( log ‘ 𝑤 ) ) )
96 89 91 95 3bitr4d ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( 𝑤 < 𝑧 ↔ - ( log ‘ 𝑤 ) ◡ < - ( log ‘ 𝑧 ) ) )
97 96 biimpd ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( 𝑤 < 𝑧 → - ( log ‘ 𝑤 ) ◡ < - ( log ‘ 𝑧 ) ) )
98 1 xrge0iifcv ⊢ ( 𝑤 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑤 ) = - ( log ‘ 𝑤 ) )
99 98 53 breqan12d ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ↔ - ( log ‘ 𝑤 ) ◡ < - ( log ‘ 𝑧 ) ) )
100 97 99 sylibrd ⊢ ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 (,] 1 ) ) → ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) )
101 84 80 100 sylc ⊢ ( ( ( 𝑤 ∈ ( 0 (,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) ∧ 𝑤 < 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) )
102 101 exp31 ⊢ ( 𝑤 ∈ ( 0 (,] 1 ) → ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) ) )
103 68 102 jaoi ⊢ ( ( 𝑤 ∈ { 0 } ∨ 𝑤 ∈ ( 0 (,] 1 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) ) )
104 24 103 sylbi ⊢ ( 𝑤 ∈ ( 0 [,] 1 ) → ( 𝑧 ∈ ( 0 [,] 1 ) → ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) ) )
105 104 imp ⊢ ( ( 𝑤 ∈ ( 0 [,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) )
106 105 rgen2 ⊢ ∀ 𝑤 ∈ ( 0 [,] 1 ) ∀ 𝑧 ∈ ( 0 [,] 1 ) ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) )
107 soisoi ⊢ ( ( ( < Or ( 0 [,] 1 ) ∧ ◡ < Po ( 0 [,] +∞ ) ) ∧ ( 𝐹 : ( 0 [,] 1 ) –onto→ ( 0 [,] +∞ ) ∧ ∀ 𝑤 ∈ ( 0 [,] 1 ) ∀ 𝑧 ∈ ( 0 [,] 1 ) ( 𝑤 < 𝑧 → ( 𝐹 ‘ 𝑤 ) ◡ < ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝐹 Isom < , ◡ < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) )
108 5 12 16 106 107 mp4an ⊢ 𝐹 Isom < , ◡ < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) )