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 ⊢ - 1 ∈ ℝ
2 1re ⊢ 1 ∈ ℝ
3 neg1lt0 ⊢ - 1 < 0
4 0lt1 ⊢ 0 < 1
5 0re ⊢ 0 ∈ ℝ
6 1 5 2 lttri ⊢ ( ( - 1 < 0 ∧ 0 < 1 ) → - 1 < 1 )
7 3 4 6 mp2an ⊢ - 1 < 1
8 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
9 eqid ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 1 ) + ( ( 1 − 𝑥 ) · - 1 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 1 ) + ( ( 1 − 𝑥 ) · - 1 ) ) )
10 8 9 icchmeo ⊢ ( ( - 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ - 1 < 1 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 1 ) + ( ( 1 − 𝑥 ) · - 1 ) ) ) ∈ ( II Homeo ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) ) )
11 1 2 7 10 mp3an ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 1 ) + ( ( 1 − 𝑥 ) · - 1 ) ) ) ∈ ( II Homeo ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) )
12 hmphi ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 1 ) + ( ( 1 − 𝑥 ) · - 1 ) ) ) ∈ ( II Homeo ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) ) → II ≃ ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) )
13 11 12 ax-mp ⊢ II ≃ ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) )
14 eqid ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) )
15 eqid ⊢ ( 𝑦 ∈ ( - 1 [,] 1 ) ↦ if ( 0 ≤ 𝑦 , ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ 𝑦 ) , -𝑒 ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ - 𝑦 ) ) ) = ( 𝑦 ∈ ( - 1 [,] 1 ) ↦ if ( 0 ≤ 𝑦 , ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ 𝑦 ) , -𝑒 ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ - 𝑦 ) ) )
16 14 15 8 xrhmeo ⊢ ( ( 𝑦 ∈ ( - 1 [,] 1 ) ↦ if ( 0 ≤ 𝑦 , ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ 𝑦 ) , -𝑒 ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ - 𝑦 ) ) ) Isom < , < ( ( - 1 [,] 1 ) , ℝ* ) ∧ ( 𝑦 ∈ ( - 1 [,] 1 ) ↦ if ( 0 ≤ 𝑦 , ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ 𝑦 ) , -𝑒 ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ - 𝑦 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) Homeo ( ordTop ‘ ≤ ) ) )
17 16 simpri ⊢ ( 𝑦 ∈ ( - 1 [,] 1 ) ↦ if ( 0 ≤ 𝑦 , ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ 𝑦 ) , -𝑒 ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ - 𝑦 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) Homeo ( ordTop ‘ ≤ ) )
18 hmphi ⊢ ( ( 𝑦 ∈ ( - 1 [,] 1 ) ↦ if ( 0 ≤ 𝑦 , ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ 𝑦 ) , -𝑒 ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 1 , +∞ , ( 𝑥 / ( 1 − 𝑥 ) ) ) ) ‘ - 𝑦 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) Homeo ( ordTop ‘ ≤ ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) ≃ ( ordTop ‘ ≤ ) )
19 17 18 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) ≃ ( ordTop ‘ ≤ )
20 hmphtr ⊢ ( ( II ≃ ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) ∧ ( ( TopOpen ‘ ℂfld ) ↾t ( - 1 [,] 1 ) ) ≃ ( ordTop ‘ ≤ ) ) → II ≃ ( ordTop ‘ ≤ ) )
21 13 19 20 mp2an ⊢ II ≃ ( ordTop ‘ ≤ )