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