# 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}=\left({x}\in \left[0,1\right]⟼if\left({x}=0,\mathrm{+\infty },-\mathrm{log}{x}\right)\right)$
Assertion xrge0iifcnv ${⊢}\left({F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right]\wedge {{F}}^{-1}=\left({y}\in \left[0,\mathrm{+\infty }\right]⟼if\left({y}=\mathrm{+\infty },0,{\mathrm{e}}^{-{y}}\right)\right)\right)$

### Proof

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