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

Metamath Proof Explorer

Theorem xrsp1

Description: The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018)

Ref Expression
Assertion xrsp1 ⊢ +∞ = 1. ⁡ ℝ 𝑠 *

Proof

Step Hyp Ref Expression
1 xrsex ⊢ ℝ 𝑠 * ∈ V
2 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
3 eqid ⊢ lub ⁡ ℝ 𝑠 * = lub ⁡ ℝ 𝑠 *
4 eqid ⊢ 1. ⁡ ℝ 𝑠 * = 1. ⁡ ℝ 𝑠 *
5 2 3 4 p1val ⊢ ℝ 𝑠 * ∈ V → 1. ⁡ ℝ 𝑠 * = lub ⁡ ℝ 𝑠 * ⁡ ℝ *
6 1 5 ax-mp ⊢ 1. ⁡ ℝ 𝑠 * = lub ⁡ ℝ 𝑠 * ⁡ ℝ *
7 ssid ⊢ ℝ * ⊆ ℝ *
8 xrslt ⊢ < = < ℝ 𝑠 *
9 xrstos ⊢ ℝ 𝑠 * ∈ Toset
10 9 a1i ⊢ ℝ * ⊆ ℝ * → ℝ 𝑠 * ∈ Toset
11 id ⊢ ℝ * ⊆ ℝ * → ℝ * ⊆ ℝ *
12 2 8 10 11 toslub ⊢ ℝ * ⊆ ℝ * → lub ⁡ ℝ 𝑠 * ⁡ ℝ * = sup ℝ * ℝ * <
13 7 12 ax-mp ⊢ lub ⁡ ℝ 𝑠 * ⁡ ℝ * = sup ℝ * ℝ * <
14 xrsup ⊢ sup ℝ * ℝ * < = +∞
15 6 13 14 3eqtrri ⊢ +∞ = 1. ⁡ ℝ 𝑠 *