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 
|- +oo = ( 1. ` RR*s )

Proof

Step Hyp Ref Expression
1 xrsex 
 |-  RR*s e. _V
2 xrsbas 
 |-  RR* = ( Base ` RR*s )
3 eqid 
 |-  ( lub ` RR*s ) = ( lub ` RR*s )
4 eqid 
 |-  ( 1. ` RR*s ) = ( 1. ` RR*s )
5 2 3 4 p1val 
 |-  ( RR*s e. _V -> ( 1. ` RR*s ) = ( ( lub ` RR*s ) ` RR* ) )
6 1 5 ax-mp 
 |-  ( 1. ` RR*s ) = ( ( lub ` RR*s ) ` RR* )
7 ssid 
 |-  RR* C_ RR*
8 xrslt 
 |-  < = ( lt ` RR*s )
9 xrstos 
 |-  RR*s e. Toset
10 9 a1i 
 |-  ( RR* C_ RR* -> RR*s e. Toset )
11 id 
 |-  ( RR* C_ RR* -> RR* C_ RR* )
12 2 8 10 11 toslub 
 |-  ( RR* C_ RR* -> ( ( lub ` RR*s ) ` RR* ) = sup ( RR* , RR* , < ) )
13 7 12 ax-mp 
 |-  ( ( lub ` RR*s ) ` RR* ) = sup ( RR* , RR* , < )
14 xrsup 
 |-  sup ( RR* , RR* , < ) = +oo
15 6 13 14 3eqtrri 
 |-  +oo = ( 1. ` RR*s )