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 𝑠*V1.𝑠*=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.𝑠*