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

Metamath Proof Explorer

Theorem xrslt

Description: The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Assertion xrslt ⊢ < = < ℝ 𝑠 *

Proof

Step Hyp Ref Expression
1 dflt2 ⊢ < = ≤ ∖ I
2 xrsex ⊢ ℝ 𝑠 * ∈ V
3 xrsle ⊢ ≤ = ≤ ℝ 𝑠 *
4 eqid ⊢ < ℝ 𝑠 * = < ℝ 𝑠 *
5 3 4 pltfval ⊢ ℝ 𝑠 * ∈ V → < ℝ 𝑠 * = ≤ ∖ I
6 2 5 ax-mp ⊢ < ℝ 𝑠 * = ≤ ∖ I
7 1 6 eqtr4i ⊢ < = < ℝ 𝑠 *