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

Metamath Proof Explorer

Theorem xrsp0

Description: The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018) (Proof shortened by AV, 28-Sep-2020)

Ref Expression
Assertion xrsp0 ⊢ −∞ = 0. ⁡ ℝ 𝑠 *

Proof

Step Hyp Ref Expression
1 xrsex ⊢ ℝ 𝑠 * ∈ V
2 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
3 eqid ⊢ glb ⁡ ℝ 𝑠 * = glb ⁡ ℝ 𝑠 *
4 eqid ⊢ 0. ⁡ ℝ 𝑠 * = 0. ⁡ ℝ 𝑠 *
5 2 3 4 p0val ⊢ ℝ 𝑠 * ∈ V → 0. ⁡ ℝ 𝑠 * = glb ⁡ ℝ 𝑠 * ⁡ ℝ *
6 1 5 ax-mp ⊢ 0. ⁡ ℝ 𝑠 * = glb ⁡ ℝ 𝑠 * ⁡ ℝ *
7 ssid ⊢ ℝ * ⊆ ℝ *
8 xrslt ⊢ < = < ℝ 𝑠 *
9 xrstos ⊢ ℝ 𝑠 * ∈ Toset
10 9 a1i ⊢ ℝ * ⊆ ℝ * → ℝ 𝑠 * ∈ Toset
11 id ⊢ ℝ * ⊆ ℝ * → ℝ * ⊆ ℝ *
12 2 8 10 11 tosglb ⊢ ℝ * ⊆ ℝ * → glb ⁡ ℝ 𝑠 * ⁡ ℝ * = inf ℝ * ℝ * <
13 7 12 ax-mp ⊢ glb ⁡ ℝ 𝑠 * ⁡ ℝ * = inf ℝ * ℝ * <
14 xrinfm ⊢ inf ℝ * ℝ * < = −∞
15 6 13 14 3eqtrri ⊢ −∞ = 0. ⁡ ℝ 𝑠 *