Metamath Proof Explorer

Theorem xrge0hmph

Description: The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Assertion xrge0hmph 
|- II ~= ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
2 eqid 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
3 1 2 iccpnfhmeo 
 |-  ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) e. ( II Homeo ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) )
4 3 simpri 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) e. ( II Homeo ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) )
5 hmphi 
 |-  ( ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) ) e. ( II Homeo ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) -> II ~= ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) )
6 4 5 ax-mp 
 |-  II ~= ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )