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 e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
Assertion xrge0iifcnv 
|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( y e. ( 0 [,] +oo ) |-> if ( y = +oo , 0 , ( exp ` -u y ) ) ) )

Proof

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