Metamath Proof Explorer

Theorem xrhmph

Description: The extended reals are homeomorphic to the interval [ 0 , 1 ] . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion xrhmph 
|- II ~= ( ordTop ` <_ )

Proof

Step Hyp Ref Expression
1 neg1rr 
 |-  -u 1 e. RR
2 1re 
 |-  1 e. RR
3 neg1lt0 
 |-  -u 1 < 0
4 0lt1 
 |-  0 < 1
5 0re 
 |-  0 e. RR
6 1 5 2 lttri 
 |-  ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 )
7 3 4 6 mp2an 
 |-  -u 1 < 1
8 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
9 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) = ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) )
10 8 9 icchmeo 
 |-  ( ( -u 1 e. RR /\ 1 e. RR /\ -u 1 < 1 ) -> ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) e. ( II Homeo ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ) )
11 1 2 7 10 mp3an 
 |-  ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) e. ( II Homeo ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) )
12 hmphi 
 |-  ( ( x e. ( 0 [,] 1 ) |-> ( ( x x. 1 ) + ( ( 1 - x ) x. -u 1 ) ) ) e. ( II Homeo ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ) -> II ~= ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) )
13 11 12 ax-mp 
 |-  II ~= ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) )
14 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
15 eqid 
 |-  ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) = ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) )
16 14 15 8 xrhmeo 
 |-  ( ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) Isom < , < ( ( -u 1 [,] 1 ) , RR* ) /\ ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) )
17 16 simpri 
 |-  ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) )
18 hmphi 
 |-  ( ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` y ) , -e ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) ` -u y ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) Homeo ( ordTop ` <_ ) ) -> ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ~= ( ordTop ` <_ ) )
19 17 18 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ~= ( ordTop ` <_ )
20 hmphtr 
 |-  ( ( II ~= ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) /\ ( ( TopOpen ` CCfld ) |`t ( -u 1 [,] 1 ) ) ~= ( ordTop ` <_ ) ) -> II ~= ( ordTop ` <_ ) )
21 13 19 20 mp2an 
 |-  II ~= ( ordTop ` <_ )