Metamath Proof Explorer

Theorem xrge0topn

Description: The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017)

Ref Expression
Assertion xrge0topn ⊢ TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞

Proof

Step Hyp Ref Expression
1 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
2 xrstopn ⊢ ordTop ⁡ ≤ = TopOpen ⁡ ℝ 𝑠 *
3 1 2 resstopn ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
4 3 eqcomi ⊢ TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞