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 ⊢x∈01⟼x⋅1+1−x⁢-1=x∈01⟼x⋅1+1−x⁢-1
10 8 9 icchmeo ⊢−1∈ℝ∧1∈ℝ∧−1<1→x∈01⟼x⋅1+1−x⁢-1∈IIHomeoTopOpen⁡ℂfld↾𝑡−11
11 1 2 7 10 mp3an ⊢x∈01⟼x⋅1+1−x⁢-1∈IIHomeoTopOpen⁡ℂfld↾𝑡−11
12 hmphi ⊢x∈01⟼x⋅1+1−x⁢-1∈IIHomeoTopOpen⁡ℂfld↾𝑡−11→II≃TopOpen⁡ℂfld↾𝑡−11
13 11 12 ax-mp ⊢II≃TopOpen⁡ℂfld↾𝑡−11
14 eqid ⊢x∈01⟼ifx=1+∞x1−x=x∈01⟼ifx=1+∞x1−x
15 eqid ⊢y∈−11⟼if0≤yx∈01⟼ifx=1+∞x1−x⁡y−x∈01⟼ifx=1+∞x1−x⁡−y=y∈−11⟼if0≤yx∈01⟼ifx=1+∞x1−x⁡y−x∈01⟼ifx=1+∞x1−x⁡−y
16 14 15 8 xrhmeo ⊢y∈−11⟼if0≤yx∈01⟼ifx=1+∞x1−x⁡y−x∈01⟼ifx=1+∞x1−x⁡−yIsom<,<−11ℝ*∧y∈−11⟼if0≤yx∈01⟼ifx=1+∞x1−x⁡y−x∈01⟼ifx=1+∞x1−x⁡−y∈TopOpen⁡ℂfld↾𝑡−11HomeoordTop⁡≤
17 16 simpri ⊢y∈−11⟼if0≤yx∈01⟼ifx=1+∞x1−x⁡y−x∈01⟼ifx=1+∞x1−x⁡−y∈TopOpen⁡ℂfld↾𝑡−11HomeoordTop⁡≤
18 hmphi ⊢y∈−11⟼if0≤yx∈01⟼ifx=1+∞x1−x⁡y−x∈01⟼ifx=1+∞x1−x⁡−y∈TopOpen⁡ℂfld↾𝑡−11HomeoordTop⁡≤→TopOpen⁡ℂfld↾𝑡−11≃ordTop⁡≤
19 17 18 ax-mp ⊢TopOpen⁡ℂfld↾𝑡−11≃ordTop⁡≤
20 hmphtr ⊢II≃TopOpen⁡ℂfld↾𝑡−11∧TopOpen⁡ℂfld↾𝑡−11≃ordTop⁡≤→II≃ordTop⁡≤
21 13 19 20 mp2an ⊢II≃ordTop⁡≤