Metamath Proof Explorer

Theorem xrge0iifcnv

Description: Define a bijection from [ 0 , 1 ] onto [ 0 , +oo ] . (Contributed by Thierry Arnoux, 29-Mar-2017)

Ref Expression
Hypothesis xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=0+∞−log⁡x
Assertion xrge0iifcnv ⊢F:01⟶1-1 onto0+∞∧F-1=y∈0+∞⟼ify=+∞0e−y

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=0+∞−log⁡x
2 0xr ⊢0∈ℝ*
3 pnfxr ⊢+∞∈ℝ*
4 0lepnf ⊢0≤+∞
5 ubicc2 ⊢0∈ℝ*∧+∞∈ℝ*∧0≤+∞→+∞∈0+∞
6 2 3 4 5 mp3an ⊢+∞∈0+∞
7 6 a1i ⊢x∈01∧x=0→+∞∈0+∞
8 icossicc ⊢0+∞⊆0+∞
9 uncom ⊢0∪01=01∪0
10 1xr ⊢1∈ℝ*
11 0le1 ⊢0≤1
12 snunioc ⊢0∈ℝ*∧1∈ℝ*∧0≤1→0∪01=01
13 2 10 11 12 mp3an ⊢0∪01=01
14 9 13 eqtr3i ⊢01∪0=01
15 14 eleq2i ⊢x∈01∪0↔x∈01
16 elun ⊢x∈01∪0↔x∈01∨x∈0
17 15 16 bitr3i ⊢x∈01↔x∈01∨x∈0
18 pm2.53 ⊢x∈01∨x∈0→¬x∈01→x∈0
19 17 18 sylbi ⊢x∈01→¬x∈01→x∈0
20 elsni ⊢x∈0→x=0
21 19 20 syl6 ⊢x∈01→¬x∈01→x=0
22 21 con1d ⊢x∈01→¬x=0→x∈01
23 22 imp ⊢x∈01∧¬x=0→x∈01
24 0le0 ⊢0≤0
25 1re ⊢1∈ℝ
26 ltpnf ⊢1∈ℝ→1<+∞
27 25 26 ax-mp ⊢1<+∞
28 iocssioo ⊢0∈ℝ*∧+∞∈ℝ*∧0≤0∧1<+∞→01⊆0+∞
29 2 3 24 27 28 mp4an ⊢01⊆0+∞
30 ioorp ⊢0+∞=ℝ+
31 29 30 sseqtri ⊢01⊆ℝ+
32 31 sseli ⊢x∈01→x∈ℝ+
33 32 relogcld ⊢x∈01→log⁡x∈ℝ
34 33 renegcld ⊢x∈01→−log⁡x∈ℝ
35 34 rexrd ⊢x∈01→−log⁡x∈ℝ*
36 elioc1 ⊢0∈ℝ*∧1∈ℝ*→x∈01↔x∈ℝ*∧0<x∧x≤1
37 2 10 36 mp2an ⊢x∈01↔x∈ℝ*∧0<x∧x≤1
38 37 simp3bi ⊢x∈01→x≤1
39 1rp ⊢1∈ℝ+
40 39 a1i ⊢x∈01→1∈ℝ+
41 32 40 logled ⊢x∈01→x≤1↔log⁡x≤log⁡1
42 38 41 mpbid ⊢x∈01→log⁡x≤log⁡1
43 log1 ⊢log⁡1=0
44 42 43 breqtrdi ⊢x∈01→log⁡x≤0
45 33 le0neg1d ⊢x∈01→log⁡x≤0↔0≤−log⁡x
46 44 45 mpbid ⊢x∈01→0≤−log⁡x
47 ltpnf ⊢−log⁡x∈ℝ→−log⁡x<+∞
48 34 47 syl ⊢x∈01→−log⁡x<+∞
49 elico1 ⊢0∈ℝ*∧+∞∈ℝ*→−log⁡x∈0+∞↔−log⁡x∈ℝ*∧0≤−log⁡x∧−log⁡x<+∞
50 2 3 49 mp2an ⊢−log⁡x∈0+∞↔−log⁡x∈ℝ*∧0≤−log⁡x∧−log⁡x<+∞
51 35 46 48 50 syl3anbrc ⊢x∈01→−log⁡x∈0+∞
52 23 51 syl ⊢x∈01∧¬x=0→−log⁡x∈0+∞
53 8 52 sselid ⊢x∈01∧¬x=0→−log⁡x∈0+∞
54 7 53 ifclda ⊢x∈01→ifx=0+∞−log⁡x∈0+∞
55 54 adantl ⊢⊤∧x∈01→ifx=0+∞−log⁡x∈0+∞
56 0elunit ⊢0∈01
57 56 a1i ⊢y∈0+∞∧y=+∞→0∈01
58 iocssicc ⊢01⊆01
59 snunico ⊢0∈ℝ*∧+∞∈ℝ*∧0≤+∞→0+∞∪+∞=0+∞
60 2 3 4 59 mp3an ⊢0+∞∪+∞=0+∞
61 60 eleq2i ⊢y∈0+∞∪+∞↔y∈0+∞
62 elun ⊢y∈0+∞∪+∞↔y∈0+∞∨y∈+∞
63 61 62 bitr3i ⊢y∈0+∞↔y∈0+∞∨y∈+∞
64 pm2.53 ⊢y∈0+∞∨y∈+∞→¬y∈0+∞→y∈+∞
65 63 64 sylbi ⊢y∈0+∞→¬y∈0+∞→y∈+∞
66 elsni ⊢y∈+∞→y=+∞
67 65 66 syl6 ⊢y∈0+∞→¬y∈0+∞→y=+∞
68 67 con1d ⊢y∈0+∞→¬y=+∞→y∈0+∞
69 68 imp ⊢y∈0+∞∧¬y=+∞→y∈0+∞
70 rge0ssre ⊢0+∞⊆ℝ
71 70 sseli ⊢y∈0+∞→y∈ℝ
72 71 renegcld ⊢y∈0+∞→−y∈ℝ
73 72 reefcld ⊢y∈0+∞→e−y∈ℝ
74 73 rexrd ⊢y∈0+∞→e−y∈ℝ*
75 efgt0 ⊢−y∈ℝ→0<e−y
76 72 75 syl ⊢y∈0+∞→0<e−y
77 elico1 ⊢0∈ℝ*∧+∞∈ℝ*→y∈0+∞↔y∈ℝ*∧0≤y∧y<+∞
78 2 3 77 mp2an ⊢y∈0+∞↔y∈ℝ*∧0≤y∧y<+∞
79 78 simp2bi ⊢y∈0+∞→0≤y
80 71 le0neg2d ⊢y∈0+∞→0≤y↔−y≤0
81 79 80 mpbid ⊢y∈0+∞→−y≤0
82 0re ⊢0∈ℝ
83 efle ⊢−y∈ℝ∧0∈ℝ→−y≤0↔e−y≤e0
84 72 82 83 sylancl ⊢y∈0+∞→−y≤0↔e−y≤e0
85 81 84 mpbid ⊢y∈0+∞→e−y≤e0
86 ef0 ⊢e0=1
87 85 86 breqtrdi ⊢y∈0+∞→e−y≤1
88 elioc1 ⊢0∈ℝ*∧1∈ℝ*→e−y∈01↔e−y∈ℝ*∧0<e−y∧e−y≤1
89 2 10 88 mp2an ⊢e−y∈01↔e−y∈ℝ*∧0<e−y∧e−y≤1
90 74 76 87 89 syl3anbrc ⊢y∈0+∞→e−y∈01
91 69 90 syl ⊢y∈0+∞∧¬y=+∞→e−y∈01
92 58 91 sselid ⊢y∈0+∞∧¬y=+∞→e−y∈01
93 57 92 ifclda ⊢y∈0+∞→ify=+∞0e−y∈01
94 93 adantl ⊢⊤∧y∈0+∞→ify=+∞0e−y∈01
95 eqeq2 ⊢0=ify=+∞0e−y→x=0↔x=ify=+∞0e−y
96 95 bibi1d ⊢0=ify=+∞0e−y→x=0↔y=ifx=0+∞−log⁡x↔x=ify=+∞0e−y↔y=ifx=0+∞−log⁡x
97 eqeq2 ⊢e−y=ify=+∞0e−y→x=e−y↔x=ify=+∞0e−y
98 97 bibi1d ⊢e−y=ify=+∞0e−y→x=e−y↔y=ifx=0+∞−log⁡x↔x=ify=+∞0e−y↔y=ifx=0+∞−log⁡x
99 simpr ⊢x∈01∧y∈0+∞∧y=+∞→y=+∞
100 iftrue ⊢x=0→ifx=0+∞−log⁡x=+∞
101 100 eqeq2d ⊢x=0→y=ifx=0+∞−log⁡x↔y=+∞
102 99 101 syl5ibrcom ⊢x∈01∧y∈0+∞∧y=+∞→x=0→y=ifx=0+∞−log⁡x
103 ubico ⊢0∈ℝ∧+∞∈ℝ*→¬+∞∈0+∞
104 82 3 103 mp2an ⊢¬+∞∈0+∞
105 104 nelir ⊢+∞∉0+∞
106 neleq1 ⊢y=+∞→y∉0+∞↔+∞∉0+∞
107 106 adantl ⊢x∈01∧y∈0+∞∧y=+∞→y∉0+∞↔+∞∉0+∞
108 105 107 mpbiri ⊢x∈01∧y∈0+∞∧y=+∞→y∉0+∞
109 neleq1 ⊢y=ifx=0+∞−log⁡x→y∉0+∞↔ifx=0+∞−log⁡x∉0+∞
110 108 109 syl5ibcom ⊢x∈01∧y∈0+∞∧y=+∞→y=ifx=0+∞−log⁡x→ifx=0+∞−log⁡x∉0+∞
111 df-nel ⊢ifx=0+∞−log⁡x∉0+∞↔¬ifx=0+∞−log⁡x∈0+∞
112 iffalse ⊢¬x=0→ifx=0+∞−log⁡x=−log⁡x
113 112 adantl ⊢x∈01∧¬x=0→ifx=0+∞−log⁡x=−log⁡x
114 113 52 eqeltrd ⊢x∈01∧¬x=0→ifx=0+∞−log⁡x∈0+∞
115 114 ex ⊢x∈01→¬x=0→ifx=0+∞−log⁡x∈0+∞
116 115 ad2antrr ⊢x∈01∧y∈0+∞∧y=+∞→¬x=0→ifx=0+∞−log⁡x∈0+∞
117 116 con1d ⊢x∈01∧y∈0+∞∧y=+∞→¬ifx=0+∞−log⁡x∈0+∞→x=0
118 111 117 biimtrid ⊢x∈01∧y∈0+∞∧y=+∞→ifx=0+∞−log⁡x∉0+∞→x=0
119 110 118 syld ⊢x∈01∧y∈0+∞∧y=+∞→y=ifx=0+∞−log⁡x→x=0
120 102 119 impbid ⊢x∈01∧y∈0+∞∧y=+∞→x=0↔y=ifx=0+∞−log⁡x
121 eqeq2 ⊢+∞=ifx=0+∞−log⁡x→y=+∞↔y=ifx=0+∞−log⁡x
122 121 bibi2d ⊢+∞=ifx=0+∞−log⁡x→x=e−y↔y=+∞↔x=e−y↔y=ifx=0+∞−log⁡x
123 eqeq2 ⊢−log⁡x=ifx=0+∞−log⁡x→y=−log⁡x↔y=ifx=0+∞−log⁡x
124 123 bibi2d ⊢−log⁡x=ifx=0+∞−log⁡x→x=e−y↔y=−log⁡x↔x=e−y↔y=ifx=0+∞−log⁡x
125 82 a1i ⊢y∈0+∞∧¬y=+∞→0∈ℝ
126 69 76 syl ⊢y∈0+∞∧¬y=+∞→0<e−y
127 125 126 ltned ⊢y∈0+∞∧¬y=+∞→0≠e−y
128 127 adantll ⊢x∈01∧y∈0+∞∧¬y=+∞→0≠e−y
129 128 neneqd ⊢x∈01∧y∈0+∞∧¬y=+∞→¬0=e−y
130 eqeq1 ⊢x=0→x=e−y↔0=e−y
131 130 notbid ⊢x=0→¬x=e−y↔¬0=e−y
132 129 131 syl5ibrcom ⊢x∈01∧y∈0+∞∧¬y=+∞→x=0→¬x=e−y
133 132 imp ⊢x∈01∧y∈0+∞∧¬y=+∞∧x=0→¬x=e−y
134 simplr ⊢x∈01∧y∈0+∞∧¬y=+∞∧x=0→¬y=+∞
135 133 134 2falsed ⊢x∈01∧y∈0+∞∧¬y=+∞∧x=0→x=e−y↔y=+∞
136 eqcom ⊢x=e−y↔e−y=x
137 136 a1i ⊢x∈01∧y∈0+∞→x=e−y↔e−y=x
138 relogeftb ⊢x∈ℝ+∧−y∈ℝ→log⁡x=−y↔e−y=x
139 32 72 138 syl2an ⊢x∈01∧y∈0+∞→log⁡x=−y↔e−y=x
140 33 recnd ⊢x∈01→log⁡x∈ℂ
141 71 recnd ⊢y∈0+∞→y∈ℂ
142 negcon2 ⊢log⁡x∈ℂ∧y∈ℂ→log⁡x=−y↔y=−log⁡x
143 140 141 142 syl2an ⊢x∈01∧y∈0+∞→log⁡x=−y↔y=−log⁡x
144 137 139 143 3bitr2d ⊢x∈01∧y∈0+∞→x=e−y↔y=−log⁡x
145 23 69 144 syl2an ⊢x∈01∧¬x=0∧y∈0+∞∧¬y=+∞→x=e−y↔y=−log⁡x
146 145 an4s ⊢x∈01∧y∈0+∞∧¬x=0∧¬y=+∞→x=e−y↔y=−log⁡x
147 146 anass1rs ⊢x∈01∧y∈0+∞∧¬y=+∞∧¬x=0→x=e−y↔y=−log⁡x
148 122 124 135 147 ifbothda ⊢x∈01∧y∈0+∞∧¬y=+∞→x=e−y↔y=ifx=0+∞−log⁡x
149 96 98 120 148 ifbothda ⊢x∈01∧y∈0+∞→x=ify=+∞0e−y↔y=ifx=0+∞−log⁡x
150 149 adantl ⊢⊤∧x∈01∧y∈0+∞→x=ify=+∞0e−y↔y=ifx=0+∞−log⁡x
151 1 55 94 150 f1ocnv2d ⊢⊤→F:01⟶1-1 onto0+∞∧F-1=y∈0+∞⟼ify=+∞0e−y
152 151 mptru ⊢F:01⟶1-1 onto0+∞∧F-1=y∈0+∞⟼ify=+∞0e−y