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 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) )
2		eqid	⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
3	1 2	iccpnfhmeo	⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ∈ ( II Homeo ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) )
4	3	simpri	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ∈ ( II Homeo ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) )
5		hmphi	⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ∈ ( II Homeo ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) → II ≃ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) )
6	4 5	ax-mp	⊢ II ≃ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )