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

Metamath Proof Explorer

Theorem xrsp0

Description: The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018) (Proof shortened by AV, 28-Sep-2020)

Ref Expression
Assertion xrsp0 
|- -oo = ( 0. ` RR*s )

Proof

Step Hyp Ref Expression
1 xrsex 
 |-  RR*s e. _V
2 xrsbas 
 |-  RR* = ( Base ` RR*s )
3 eqid 
 |-  ( glb ` RR*s ) = ( glb ` RR*s )
4 eqid 
 |-  ( 0. ` RR*s ) = ( 0. ` RR*s )
5 2 3 4 p0val 
 |-  ( RR*s e. _V -> ( 0. ` RR*s ) = ( ( glb ` RR*s ) ` RR* ) )
6 1 5 ax-mp 
 |-  ( 0. ` RR*s ) = ( ( glb ` 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 tosglb 
 |-  ( RR* C_ RR* -> ( ( glb ` RR*s ) ` RR* ) = inf ( RR* , RR* , < ) )
13 7 12 ax-mp 
 |-  ( ( glb ` RR*s ) ` RR* ) = inf ( RR* , RR* , < )
14 xrinfm 
 |-  inf ( RR* , RR* , < ) = -oo
15 6 13 14 3eqtrri 
 |-  -oo = ( 0. ` RR*s )