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