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 )