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 e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
Assertion xrge0iifiso
|- F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1
 |-  F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
2 iccssxr
 |-  ( 0 [,] 1 ) C_ RR*
3 xrltso
 |-  < Or RR*
4 soss
 |-  ( ( 0 [,] 1 ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] 1 ) ) )
5 2 3 4 mp2
 |-  < Or ( 0 [,] 1 )
6 iccssxr
 |-  ( 0 [,] +oo ) C_ RR*
7 cnvso
 |-  ( < Or RR* <-> `' < Or RR* )
8 3 7 mpbi
 |-  `' < Or RR*
9 sopo
 |-  ( `' < Or RR* -> `' < Po RR* )
10 8 9 ax-mp
 |-  `' < Po RR*
11 poss
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( `' < Po RR* -> `' < Po ( 0 [,] +oo ) ) )
12 6 10 11 mp2
 |-  `' < Po ( 0 [,] +oo )
13 1 xrge0iifcnv
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( z e. ( 0 [,] +oo ) |-> if ( z = +oo , 0 , ( exp ` -u z ) ) ) )
14 13 simpli
 |-  F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )
15 f1ofo
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> F : ( 0 [,] 1 ) -onto-> ( 0 [,] +oo ) )
16 14 15 ax-mp
 |-  F : ( 0 [,] 1 ) -onto-> ( 0 [,] +oo )
17 0xr
 |-  0 e. RR*
18 1xr
 |-  1 e. RR*
19 0le1
 |-  0 <_ 1
20 snunioc
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ 0 <_ 1 ) -> ( { 0 } u. ( 0 (,] 1 ) ) = ( 0 [,] 1 ) )
21 17 18 19 20 mp3an
 |-  ( { 0 } u. ( 0 (,] 1 ) ) = ( 0 [,] 1 )
22 21 eleq2i
 |-  ( w e. ( { 0 } u. ( 0 (,] 1 ) ) <-> w e. ( 0 [,] 1 ) )
23 elun
 |-  ( w e. ( { 0 } u. ( 0 (,] 1 ) ) <-> ( w e. { 0 } \/ w e. ( 0 (,] 1 ) ) )
24 22 23 bitr3i
 |-  ( w e. ( 0 [,] 1 ) <-> ( w e. { 0 } \/ w e. ( 0 (,] 1 ) ) )
25 velsn
 |-  ( w e. { 0 } <-> w = 0 )
26 elunitrn
 |-  ( z e. ( 0 [,] 1 ) -> z e. RR )
27 26 adantr
 |-  ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> z e. RR )
28 simpr
 |-  ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> 0 < z )
29 elicc01
 |-  ( z e. ( 0 [,] 1 ) <-> ( z e. RR /\ 0 <_ z /\ z <_ 1 ) )
30 29 simp3bi
 |-  ( z e. ( 0 [,] 1 ) -> z <_ 1 )
31 30 adantr
 |-  ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> z <_ 1 )
32 1re
 |-  1 e. RR
33 elioc2
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( z e. ( 0 (,] 1 ) <-> ( z e. RR /\ 0 < z /\ z <_ 1 ) ) )
34 17 32 33 mp2an
 |-  ( z e. ( 0 (,] 1 ) <-> ( z e. RR /\ 0 < z /\ z <_ 1 ) )
35 27 28 31 34 syl3anbrc
 |-  ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> z e. ( 0 (,] 1 ) )
36 pnfxr
 |-  +oo e. RR*
37 0le0
 |-  0 <_ 0
38 ltpnf
 |-  ( 1 e. RR -> 1 < +oo )
39 32 38 ax-mp
 |-  1 < +oo
40 iocssioo
 |-  ( ( ( 0 e. RR* /\ +oo e. RR* ) /\ ( 0 <_ 0 /\ 1 < +oo ) ) -> ( 0 (,] 1 ) C_ ( 0 (,) +oo ) )
41 17 36 37 39 40 mp4an
 |-  ( 0 (,] 1 ) C_ ( 0 (,) +oo )
42 ioorp
 |-  ( 0 (,) +oo ) = RR+
43 41 42 sseqtri
 |-  ( 0 (,] 1 ) C_ RR+
44 43 sseli
 |-  ( z e. ( 0 (,] 1 ) -> z e. RR+ )
45 relogcl
 |-  ( z e. RR+ -> ( log ` z ) e. RR )
46 45 renegcld
 |-  ( z e. RR+ -> -u ( log ` z ) e. RR )
47 ltpnf
 |-  ( -u ( log ` z ) e. RR -> -u ( log ` z ) < +oo )
48 46 47 syl
 |-  ( z e. RR+ -> -u ( log ` z ) < +oo )
49 brcnvg
 |-  ( ( +oo e. RR* /\ -u ( log ` z ) e. RR ) -> ( +oo `' < -u ( log ` z ) <-> -u ( log ` z ) < +oo ) )
50 36 46 49 sylancr
 |-  ( z e. RR+ -> ( +oo `' < -u ( log ` z ) <-> -u ( log ` z ) < +oo ) )
51 48 50 mpbird
 |-  ( z e. RR+ -> +oo `' < -u ( log ` z ) )
52 44 51 syl
 |-  ( z e. ( 0 (,] 1 ) -> +oo `' < -u ( log ` z ) )
53 1 xrge0iifcv
 |-  ( z e. ( 0 (,] 1 ) -> ( F ` z ) = -u ( log ` z ) )
54 52 53 breqtrrd
 |-  ( z e. ( 0 (,] 1 ) -> +oo `' < ( F ` z ) )
55 35 54 syl
 |-  ( ( z e. ( 0 [,] 1 ) /\ 0 < z ) -> +oo `' < ( F ` z ) )
56 55 ex
 |-  ( z e. ( 0 [,] 1 ) -> ( 0 < z -> +oo `' < ( F ` z ) ) )
57 breq1
 |-  ( w = 0 -> ( w < z <-> 0 < z ) )
58 fveq2
 |-  ( w = 0 -> ( F ` w ) = ( F ` 0 ) )
59 0elunit
 |-  0 e. ( 0 [,] 1 )
60 iftrue
 |-  ( x = 0 -> if ( x = 0 , +oo , -u ( log ` x ) ) = +oo )
61 pnfex
 |-  +oo e. _V
62 60 1 61 fvmpt
 |-  ( 0 e. ( 0 [,] 1 ) -> ( F ` 0 ) = +oo )
63 59 62 ax-mp
 |-  ( F ` 0 ) = +oo
64 58 63 eqtrdi
 |-  ( w = 0 -> ( F ` w ) = +oo )
65 64 breq1d
 |-  ( w = 0 -> ( ( F ` w ) `' < ( F ` z ) <-> +oo `' < ( F ` z ) ) )
66 57 65 imbi12d
 |-  ( w = 0 -> ( ( w < z -> ( F ` w ) `' < ( F ` z ) ) <-> ( 0 < z -> +oo `' < ( F ` z ) ) ) )
67 56 66 syl5ibr
 |-  ( w = 0 -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) )
68 25 67 sylbi
 |-  ( w e. { 0 } -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) )
69 simpll
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> w e. ( 0 (,] 1 ) )
70 26 ad2antlr
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> z e. RR )
71 0re
 |-  0 e. RR
72 71 a1i
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> 0 e. RR )
73 43 sseli
 |-  ( w e. ( 0 (,] 1 ) -> w e. RR+ )
74 73 rpred
 |-  ( w e. ( 0 (,] 1 ) -> w e. RR )
75 74 ad2antrr
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> w e. RR )
76 elioc2
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( w e. ( 0 (,] 1 ) <-> ( w e. RR /\ 0 < w /\ w <_ 1 ) ) )
77 17 32 76 mp2an
 |-  ( w e. ( 0 (,] 1 ) <-> ( w e. RR /\ 0 < w /\ w <_ 1 ) )
78 77 simp2bi
 |-  ( w e. ( 0 (,] 1 ) -> 0 < w )
79 78 ad2antrr
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> 0 < w )
80 simpr
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> w < z )
81 72 75 70 79 80 lttrd
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> 0 < z )
82 30 ad2antlr
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> z <_ 1 )
83 70 81 82 34 syl3anbrc
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> z e. ( 0 (,] 1 ) )
84 69 83 jca
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) )
85 73 adantr
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> w e. RR+ )
86 85 relogcld
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( log ` w ) e. RR )
87 44 adantl
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> z e. RR+ )
88 87 relogcld
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( log ` z ) e. RR )
89 86 88 ltnegd
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( ( log ` w ) < ( log ` z ) <-> -u ( log ` z ) < -u ( log ` w ) ) )
90 logltb
 |-  ( ( w e. RR+ /\ z e. RR+ ) -> ( w < z <-> ( log ` w ) < ( log ` z ) ) )
91 73 44 90 syl2an
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z <-> ( log ` w ) < ( log ` z ) ) )
92 negex
 |-  -u ( log ` w ) e. _V
93 negex
 |-  -u ( log ` z ) e. _V
94 92 93 brcnv
 |-  ( -u ( log ` w ) `' < -u ( log ` z ) <-> -u ( log ` z ) < -u ( log ` w ) )
95 94 a1i
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( -u ( log ` w ) `' < -u ( log ` z ) <-> -u ( log ` z ) < -u ( log ` w ) ) )
96 89 91 95 3bitr4d
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z <-> -u ( log ` w ) `' < -u ( log ` z ) ) )
97 96 biimpd
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z -> -u ( log ` w ) `' < -u ( log ` z ) ) )
98 1 xrge0iifcv
 |-  ( w e. ( 0 (,] 1 ) -> ( F ` w ) = -u ( log ` w ) )
99 98 53 breqan12d
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( ( F ` w ) `' < ( F ` z ) <-> -u ( log ` w ) `' < -u ( log ` z ) ) )
100 97 99 sylibrd
 |-  ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 (,] 1 ) ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) )
101 84 80 100 sylc
 |-  ( ( ( w e. ( 0 (,] 1 ) /\ z e. ( 0 [,] 1 ) ) /\ w < z ) -> ( F ` w ) `' < ( F ` z ) )
102 101 exp31
 |-  ( w e. ( 0 (,] 1 ) -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) )
103 68 102 jaoi
 |-  ( ( w e. { 0 } \/ w e. ( 0 (,] 1 ) ) -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) )
104 24 103 sylbi
 |-  ( w e. ( 0 [,] 1 ) -> ( z e. ( 0 [,] 1 ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) )
105 104 imp
 |-  ( ( w e. ( 0 [,] 1 ) /\ z e. ( 0 [,] 1 ) ) -> ( w < z -> ( F ` w ) `' < ( F ` z ) ) )
106 105 rgen2
 |-  A. w e. ( 0 [,] 1 ) A. z e. ( 0 [,] 1 ) ( w < z -> ( F ` w ) `' < ( F ` z ) )
107 soisoi
 |-  ( ( ( < Or ( 0 [,] 1 ) /\ `' < Po ( 0 [,] +oo ) ) /\ ( F : ( 0 [,] 1 ) -onto-> ( 0 [,] +oo ) /\ A. w e. ( 0 [,] 1 ) A. z e. ( 0 [,] 1 ) ( w < z -> ( F ` w ) `' < ( F ` z ) ) ) ) -> F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) )
108 5 12 16 106 107 mp4an
 |-  F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )