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∈01⟼ifx=0+∞−log⁡x
Assertion xrge0iifiso ⊢FIsom<,<-1010+∞

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=0+∞−log⁡x
2 iccssxr ⊢01⊆ℝ*
3 xrltso ⊢<Orℝ*
4 soss ⊢01⊆ℝ*→<Orℝ*→<Or01
5 2 3 4 mp2 ⊢<Or01
6 iccssxr ⊢0+∞⊆ℝ*
7 cnvso ⊢<Orℝ*↔<-1Orℝ*
8 3 7 mpbi ⊢<-1Orℝ*
9 sopo ⊢<-1Orℝ*→<-1Poℝ*
10 8 9 ax-mp ⊢<-1Poℝ*
11 poss ⊢0+∞⊆ℝ*→<-1Poℝ*→<-1Po0+∞
12 6 10 11 mp2 ⊢<-1Po0+∞
13 1 xrge0iifcnv ⊢F:01⟶1-1 onto0+∞∧F-1=z∈0+∞⟼ifz=+∞0e−z
14 13 simpli ⊢F:01⟶1-1 onto0+∞
15 f1ofo ⊢F:01⟶1-1 onto0+∞→F:01⟶onto0+∞
16 14 15 ax-mp ⊢F:01⟶onto0+∞
17 0xr ⊢0∈ℝ*
18 1xr ⊢1∈ℝ*
19 0le1 ⊢0≤1
20 snunioc ⊢0∈ℝ*∧1∈ℝ*∧0≤1→0∪01=01
21 17 18 19 20 mp3an ⊢0∪01=01
22 21 eleq2i ⊢w∈0∪01↔w∈01
23 elun ⊢w∈0∪01↔w∈0∨w∈01
24 22 23 bitr3i ⊢w∈01↔w∈0∨w∈01
25 velsn ⊢w∈0↔w=0
26 elunitrn ⊢z∈01→z∈ℝ
27 26 adantr ⊢z∈01∧0<z→z∈ℝ
28 simpr ⊢z∈01∧0<z→0<z
29 elicc01 ⊢z∈01↔z∈ℝ∧0≤z∧z≤1
30 29 simp3bi ⊢z∈01→z≤1
31 30 adantr ⊢z∈01∧0<z→z≤1
32 1re ⊢1∈ℝ
33 elioc2 ⊢0∈ℝ*∧1∈ℝ→z∈01↔z∈ℝ∧0<z∧z≤1
34 17 32 33 mp2an ⊢z∈01↔z∈ℝ∧0<z∧z≤1
35 27 28 31 34 syl3anbrc ⊢z∈01∧0<z→z∈01
36 pnfxr ⊢+∞∈ℝ*
37 0le0 ⊢0≤0
38 ltpnf ⊢1∈ℝ→1<+∞
39 32 38 ax-mp ⊢1<+∞
40 iocssioo ⊢0∈ℝ*∧+∞∈ℝ*∧0≤0∧1<+∞→01⊆0+∞
41 17 36 37 39 40 mp4an ⊢01⊆0+∞
42 ioorp ⊢0+∞=ℝ+
43 41 42 sseqtri ⊢01⊆ℝ+
44 43 sseli ⊢z∈01→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∈01→+∞<-1−log⁡z
53 1 xrge0iifcv ⊢z∈01→F⁡z=−log⁡z
54 52 53 breqtrrd ⊢z∈01→+∞<-1F⁡z
55 35 54 syl ⊢z∈01∧0<z→+∞<-1F⁡z
56 55 ex ⊢z∈01→0<z→+∞<-1F⁡z
57 breq1 ⊢w=0→w<z↔0<z
58 fveq2 ⊢w=0→F⁡w=F⁡0
59 0elunit ⊢0∈01
60 iftrue ⊢x=0→ifx=0+∞−log⁡x=+∞
61 pnfex ⊢+∞∈V
62 60 1 61 fvmpt ⊢0∈01→F⁡0=+∞
63 59 62 ax-mp ⊢F⁡0=+∞
64 58 63 eqtrdi ⊢w=0→F⁡w=+∞
65 64 breq1d ⊢w=0→F⁡w<-1F⁡z↔+∞<-1F⁡z
66 57 65 imbi12d ⊢w=0→w<z→F⁡w<-1F⁡z↔0<z→+∞<-1F⁡z
67 56 66 imbitrrid ⊢w=0→z∈01→w<z→F⁡w<-1F⁡z
68 25 67 sylbi ⊢w∈0→z∈01→w<z→F⁡w<-1F⁡z
69 simpll ⊢w∈01∧z∈01∧w<z→w∈01
70 26 ad2antlr ⊢w∈01∧z∈01∧w<z→z∈ℝ
71 0re ⊢0∈ℝ
72 71 a1i ⊢w∈01∧z∈01∧w<z→0∈ℝ
73 43 sseli ⊢w∈01→w∈ℝ+
74 73 rpred ⊢w∈01→w∈ℝ
75 74 ad2antrr ⊢w∈01∧z∈01∧w<z→w∈ℝ
76 elioc2 ⊢0∈ℝ*∧1∈ℝ→w∈01↔w∈ℝ∧0<w∧w≤1
77 17 32 76 mp2an ⊢w∈01↔w∈ℝ∧0<w∧w≤1
78 77 simp2bi ⊢w∈01→0<w
79 78 ad2antrr ⊢w∈01∧z∈01∧w<z→0<w
80 simpr ⊢w∈01∧z∈01∧w<z→w<z
81 72 75 70 79 80 lttrd ⊢w∈01∧z∈01∧w<z→0<z
82 30 ad2antlr ⊢w∈01∧z∈01∧w<z→z≤1
83 70 81 82 34 syl3anbrc ⊢w∈01∧z∈01∧w<z→z∈01
84 69 83 jca ⊢w∈01∧z∈01∧w<z→w∈01∧z∈01
85 73 adantr ⊢w∈01∧z∈01→w∈ℝ+
86 85 relogcld ⊢w∈01∧z∈01→log⁡w∈ℝ
87 44 adantl ⊢w∈01∧z∈01→z∈ℝ+
88 87 relogcld ⊢w∈01∧z∈01→log⁡z∈ℝ
89 86 88 ltnegd ⊢w∈01∧z∈01→log⁡w<log⁡z↔−log⁡z<−log⁡w
90 logltb ⊢w∈ℝ+∧z∈ℝ+→w<z↔log⁡w<log⁡z
91 73 44 90 syl2an ⊢w∈01∧z∈01→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∈01∧z∈01→−log⁡w<-1−log⁡z↔−log⁡z<−log⁡w
96 89 91 95 3bitr4d ⊢w∈01∧z∈01→w<z↔−log⁡w<-1−log⁡z
97 96 biimpd ⊢w∈01∧z∈01→w<z→−log⁡w<-1−log⁡z
98 1 xrge0iifcv ⊢w∈01→F⁡w=−log⁡w
99 98 53 breqan12d ⊢w∈01∧z∈01→F⁡w<-1F⁡z↔−log⁡w<-1−log⁡z
100 97 99 sylibrd ⊢w∈01∧z∈01→w<z→F⁡w<-1F⁡z
101 84 80 100 sylc ⊢w∈01∧z∈01∧w<z→F⁡w<-1F⁡z
102 101 exp31 ⊢w∈01→z∈01→w<z→F⁡w<-1F⁡z
103 68 102 jaoi ⊢w∈0∨w∈01→z∈01→w<z→F⁡w<-1F⁡z
104 24 103 sylbi ⊢w∈01→z∈01→w<z→F⁡w<-1F⁡z
105 104 imp ⊢w∈01∧z∈01→w<z→F⁡w<-1F⁡z
106 105 rgen2 ⊢∀w∈01∀z∈01w<z→F⁡w<-1F⁡z
107 soisoi ⊢<Or01∧<-1Po0+∞∧F:01⟶onto0+∞∧∀w∈01∀z∈01w<z→F⁡w<-1F⁡z→FIsom<,<-1010+∞
108 5 12 16 106 107 mp4an ⊢FIsom<,<-1010+∞