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 ⊢ F = x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
Assertion xrge0iifiso ⊢ F Isom < , < -1 0 1 0 +∞

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ F = x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
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 ℝ * ↔ < -1 Or ℝ *
8 3 7 mpbi ⊢ < -1 Or ℝ *
9 sopo ⊢ < -1 Or ℝ * → < -1 Po ℝ *
10 8 9 ax-mp ⊢ < -1 Po ℝ *
11 poss ⊢ 0 +∞ ⊆ ℝ * → < -1 Po ℝ * → < -1 Po 0 +∞
12 6 10 11 mp2 ⊢ < -1 Po 0 +∞
13 1 xrge0iifcnv ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ F -1 = z ∈ 0 +∞ ⟼ if z = +∞ 0 e − z
14 13 simpli ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞
15 f1ofo ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ → F : 0 1 ⟶ onto 0 +∞
16 14 15 ax-mp ⊢ F : 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 ⊢ w ∈ 0 ∪ 0 1 ↔ w ∈ 0 1
23 elun ⊢ w ∈ 0 ∪ 0 1 ↔ w ∈ 0 ∨ w ∈ 0 1
24 22 23 bitr3i ⊢ w ∈ 0 1 ↔ w ∈ 0 ∨ w ∈ 0 1
25 velsn ⊢ w ∈ 0 ↔ w = 0
26 elunitrn ⊢ z ∈ 0 1 → z ∈ ℝ
27 26 adantr ⊢ z ∈ 0 1 ∧ 0 < z → z ∈ ℝ
28 simpr ⊢ z ∈ 0 1 ∧ 0 < z → 0 < z
29 elicc01 ⊢ z ∈ 0 1 ↔ z ∈ ℝ ∧ 0 ≤ z ∧ z ≤ 1
30 29 simp3bi ⊢ z ∈ 0 1 → z ≤ 1
31 30 adantr ⊢ z ∈ 0 1 ∧ 0 < z → z ≤ 1
32 1re ⊢ 1 ∈ ℝ
33 elioc2 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ → z ∈ 0 1 ↔ z ∈ ℝ ∧ 0 < z ∧ z ≤ 1
34 17 32 33 mp2an ⊢ z ∈ 0 1 ↔ z ∈ ℝ ∧ 0 < z ∧ z ≤ 1
35 27 28 31 34 syl3anbrc ⊢ z ∈ 0 1 ∧ 0 < z → z ∈ 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 ⊢ z ∈ 0 1 → z ∈ ℝ +
45 relogcl ⊢ z ∈ ℝ + → log ⁡ z ∈ ℝ
46 45 renegcld ⊢ z ∈ ℝ + → − log ⁡ z ∈ ℝ
47 ltpnf ⊢ − log ⁡ z ∈ ℝ → − log ⁡ z < +∞
48 46 47 syl ⊢ z ∈ ℝ + → − log ⁡ z < +∞
49 brcnvg ⊢ +∞ ∈ ℝ * ∧ − log ⁡ z ∈ ℝ → +∞ < -1 − log ⁡ z ↔ − log ⁡ z < +∞
50 36 46 49 sylancr ⊢ z ∈ ℝ + → +∞ < -1 − log ⁡ z ↔ − log ⁡ z < +∞
51 48 50 mpbird ⊢ z ∈ ℝ + → +∞ < -1 − log ⁡ z
52 44 51 syl ⊢ z ∈ 0 1 → +∞ < -1 − log ⁡ z
53 1 xrge0iifcv ⊢ z ∈ 0 1 → F ⁡ z = − log ⁡ z
54 52 53 breqtrrd ⊢ z ∈ 0 1 → +∞ < -1 F ⁡ z
55 35 54 syl ⊢ z ∈ 0 1 ∧ 0 < z → +∞ < -1 F ⁡ z
56 55 ex ⊢ z ∈ 0 1 → 0 < z → +∞ < -1 F ⁡ z
57 breq1 ⊢ w = 0 → w < z ↔ 0 < z
58 fveq2 ⊢ w = 0 → F ⁡ w = F ⁡ 0
59 0elunit ⊢ 0 ∈ 0 1
60 iftrue ⊢ x = 0 → if x = 0 +∞ − log ⁡ x = +∞
61 pnfex ⊢ +∞ ∈ V
62 60 1 61 fvmpt ⊢ 0 ∈ 0 1 → F ⁡ 0 = +∞
63 59 62 ax-mp ⊢ F ⁡ 0 = +∞
64 58 63 eqtrdi ⊢ w = 0 → F ⁡ w = +∞
65 64 breq1d ⊢ w = 0 → F ⁡ w < -1 F ⁡ z ↔ +∞ < -1 F ⁡ z
66 57 65 imbi12d ⊢ w = 0 → w < z → F ⁡ w < -1 F ⁡ z ↔ 0 < z → +∞ < -1 F ⁡ z
67 56 66 imbitrrid ⊢ w = 0 → z ∈ 0 1 → w < z → F ⁡ w < -1 F ⁡ z
68 25 67 sylbi ⊢ w ∈ 0 → z ∈ 0 1 → w < z → F ⁡ w < -1 F ⁡ z
69 simpll ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → w ∈ 0 1
70 26 ad2antlr ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → z ∈ ℝ
71 0re ⊢ 0 ∈ ℝ
72 71 a1i ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → 0 ∈ ℝ
73 43 sseli ⊢ w ∈ 0 1 → w ∈ ℝ +
74 73 rpred ⊢ w ∈ 0 1 → w ∈ ℝ
75 74 ad2antrr ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → w ∈ ℝ
76 elioc2 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ → w ∈ 0 1 ↔ w ∈ ℝ ∧ 0 < w ∧ w ≤ 1
77 17 32 76 mp2an ⊢ w ∈ 0 1 ↔ w ∈ ℝ ∧ 0 < w ∧ w ≤ 1
78 77 simp2bi ⊢ w ∈ 0 1 → 0 < w
79 78 ad2antrr ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → 0 < w
80 simpr ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → w < z
81 72 75 70 79 80 lttrd ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → 0 < z
82 30 ad2antlr ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → z ≤ 1
83 70 81 82 34 syl3anbrc ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → z ∈ 0 1
84 69 83 jca ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → w ∈ 0 1 ∧ z ∈ 0 1
85 73 adantr ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → w ∈ ℝ +
86 85 relogcld ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → log ⁡ w ∈ ℝ
87 44 adantl ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → z ∈ ℝ +
88 87 relogcld ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → log ⁡ z ∈ ℝ
89 86 88 ltnegd ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → log ⁡ w < log ⁡ z ↔ − log ⁡ z < − log ⁡ w
90 logltb ⊢ w ∈ ℝ + ∧ z ∈ ℝ + → w < z ↔ log ⁡ w < log ⁡ z
91 73 44 90 syl2an ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → w < z ↔ log ⁡ w < log ⁡ z
92 negex ⊢ − log ⁡ w ∈ V
93 negex ⊢ − log ⁡ z ∈ V
94 92 93 brcnv ⊢ − log ⁡ w < -1 − log ⁡ z ↔ − log ⁡ z < − log ⁡ w
95 94 a1i ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → − log ⁡ w < -1 − log ⁡ z ↔ − log ⁡ z < − log ⁡ w
96 89 91 95 3bitr4d ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → w < z ↔ − log ⁡ w < -1 − log ⁡ z
97 96 biimpd ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → w < z → − log ⁡ w < -1 − log ⁡ z
98 1 xrge0iifcv ⊢ w ∈ 0 1 → F ⁡ w = − log ⁡ w
99 98 53 breqan12d ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → F ⁡ w < -1 F ⁡ z ↔ − log ⁡ w < -1 − log ⁡ z
100 97 99 sylibrd ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → w < z → F ⁡ w < -1 F ⁡ z
101 84 80 100 sylc ⊢ w ∈ 0 1 ∧ z ∈ 0 1 ∧ w < z → F ⁡ w < -1 F ⁡ z
102 101 exp31 ⊢ w ∈ 0 1 → z ∈ 0 1 → w < z → F ⁡ w < -1 F ⁡ z
103 68 102 jaoi ⊢ w ∈ 0 ∨ w ∈ 0 1 → z ∈ 0 1 → w < z → F ⁡ w < -1 F ⁡ z
104 24 103 sylbi ⊢ w ∈ 0 1 → z ∈ 0 1 → w < z → F ⁡ w < -1 F ⁡ z
105 104 imp ⊢ w ∈ 0 1 ∧ z ∈ 0 1 → w < z → F ⁡ w < -1 F ⁡ z
106 105 rgen2 ⊢ ∀ w ∈ 0 1 ∀ z ∈ 0 1 w < z → F ⁡ w < -1 F ⁡ z
107 soisoi ⊢ < Or 0 1 ∧ < -1 Po 0 +∞ ∧ F : 0 1 ⟶ onto 0 +∞ ∧ ∀ w ∈ 0 1 ∀ z ∈ 0 1 w < z → F ⁡ w < -1 F ⁡ z → F Isom < , < -1 0 1 0 +∞
108 5 12 16 106 107 mp4an ⊢ F Isom < , < -1 0 1 0 +∞