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

Metamath Proof Explorer

Theorem xrge0le

Description: The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018)

Ref Expression
Assertion xrge0le ⊢ ≤ = ≤ ℝ 𝑠 * ↾ 𝑠 0 +∞

Proof

Step Hyp Ref Expression
1 ovex ⊢ 0 +∞ ∈ V
2 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
3 xrsle ⊢ ≤ = ≤ ℝ 𝑠 *
4 2 3 ressle ⊢ 0 +∞ ∈ V → ≤ = ≤ ℝ 𝑠 * ↾ 𝑠 0 +∞
5 1 4 ax-mp ⊢ ≤ = ≤ ℝ 𝑠 * ↾ 𝑠 0 +∞