Metamath Proof Explorer

Theorem xrge0iifhmeo

Description: Expose a homeomorphism from the closed unit interval to the extended nonnegative reals. (Contributed by Thierry Arnoux, 1-Apr-2017)

Ref Expression
Hypotheses xrge0iifhmeo.1 
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
xrge0iifhmeo.k 
|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
Assertion xrge0iifhmeo 
|- F e. ( II Homeo J )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 
 |-  F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
2 xrge0iifhmeo.k 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
3 letsr 
 |-  <_ e. TosetRel
4 tsrps 
 |-  ( <_ e. TosetRel -> <_ e. PosetRel )
5 3 4 ax-mp 
 |-  <_ e. PosetRel
6 5 elexi 
 |-  <_ e. _V
7 6 inex1 
 |-  ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. _V
8 cnvps 
 |-  ( <_ e. PosetRel -> `' <_ e. PosetRel )
9 5 8 ax-mp 
 |-  `' <_ e. PosetRel
10 9 elexi 
 |-  `' <_ e. _V
11 10 inex1 
 |-  ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) e. _V
12 1 xrge0iifiso 
 |-  F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )
13 iccssxr 
 |-  ( 0 [,] 1 ) C_ RR*
14 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
15 gtiso 
 |-  ( ( ( 0 [,] 1 ) C_ RR* /\ ( 0 [,] +oo ) C_ RR* ) -> ( F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) <-> F Isom <_ , `' <_ ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) ) )
16 13 14 15 mp2an 
 |-  ( F Isom < , `' < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) <-> F Isom <_ , `' <_ ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) )
17 12 16 mpbi 
 |-  F Isom <_ , `' <_ ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )
18 isores1 
 |-  ( F Isom <_ , `' <_ ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) <-> F Isom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) , `' <_ ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) )
19 17 18 mpbi 
 |-  F Isom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) , `' <_ ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )
20 isores2 
 |-  ( F Isom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) , `' <_ ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) <-> F Isom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) , ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) )
21 19 20 mpbi 
 |-  F Isom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) , ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )
22 ledm 
 |-  RR* = dom <_
23 22 psssdm 
 |-  ( ( <_ e. PosetRel /\ ( 0 [,] 1 ) C_ RR* ) -> dom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) = ( 0 [,] 1 ) )
24 5 13 23 mp2an 
 |-  dom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) = ( 0 [,] 1 )
25 24 eqcomi 
 |-  ( 0 [,] 1 ) = dom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
26 lern 
 |-  RR* = ran <_
27 df-rn 
 |-  ran <_ = dom `' <_
28 26 27 eqtri 
 |-  RR* = dom `' <_
29 28 psssdm 
 |-  ( ( `' <_ e. PosetRel /\ ( 0 [,] +oo ) C_ RR* ) -> dom ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) = ( 0 [,] +oo ) )
30 9 14 29 mp2an 
 |-  dom ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) = ( 0 [,] +oo )
31 30 eqcomi 
 |-  ( 0 [,] +oo ) = dom ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) )
32 25 31 ordthmeo 
 |-  ( ( ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. _V /\ ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) e. _V /\ F Isom ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) , ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) ) -> F e. ( ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) ) Homeo ( ordTop ` ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ) ) )
33 7 11 21 32 mp3an 
 |-  F e. ( ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) ) Homeo ( ordTop ` ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ) )
34 dfii5 
 |-  II = ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
35 iccss2 
 |-  ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( x [,] y ) C_ ( 0 [,] +oo ) )
36 14 35 cnvordtrestixx 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( ordTop ` ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) )
37 2 36 eqtri 
 |-  J = ( ordTop ` ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) )
38 34 37 oveq12i 
 |-  ( II Homeo J ) = ( ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) ) Homeo ( ordTop ` ( `' <_ i^i ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ) )
39 33 38 eleqtrri 
 |-  F e. ( II Homeo J )