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 sselid
 |-  ( ( 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 sselid
 |-  ( ( 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 ) ) ) )