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 ⁡ ≤ ↾ 𝑡 0 +∞

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x = x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x
2 eqid ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
3 1 2 iccpnfhmeo ⊢ x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x Isom < , < 0 1 0 +∞ ∧ x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x ∈ II Homeo ordTop ⁡ ≤ ↾ 𝑡 0 +∞
4 3 simpri ⊢ x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x ∈ II Homeo ordTop ⁡ ≤ ↾ 𝑡 0 +∞
5 hmphi ⊢ x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x ∈ II Homeo ordTop ⁡ ≤ ↾ 𝑡 0 +∞ → II ≃ ordTop ⁡ ≤ ↾ 𝑡 0 +∞
6 4 5 ax-mp ⊢ II ≃ ordTop ⁡ ≤ ↾ 𝑡 0 +∞