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 ⊢ < = ( lt ‘ ℝ*𝑠 )
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. ‘ ℝ*𝑠 )