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 )