This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reordt

Description: The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion reordt ⊢ ℝ ∈ ordTop ⁡ ≤

Proof

Step Hyp Ref Expression
1 ioomax ⊢ −∞ +∞ = ℝ
2 iooordt ⊢ −∞ +∞ ∈ ordTop ⁡ ≤
3 1 2 eqeltrri ⊢ ℝ ∈ ordTop ⁡ ≤