Theorem xrge0omnd

Description: The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018)

	Ref	Expression
Assertion	xrge0omnd	|- ( RR*s |`s ( 0 [,] +oo ) ) e. oMnd

Proof

Step	Hyp	Ref	Expression
1		xrge0cmn	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
2		cmnmnd	|- ( ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
3	1 2	ax-mp	|- ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
4		ovex	|- ( RR*s |`s ( 0 [,] +oo ) ) e. _V
5		xrge0base	|- ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
6		xrge0le	|- <_ = ( le ` ( RR*s |`s ( 0 [,] +oo ) ) )
7		eliccxr	|- ( x e. ( 0 [,] +oo ) -> x e. RR* )
8	7	xrleidd	|- ( x e. ( 0 [,] +oo ) -> x <_ x )
9		eliccxr	|- ( y e. ( 0 [,] +oo ) -> y e. RR* )
10		xrletri3	|- ( ( x e. RR* /\ y e. RR* ) -> ( x = y <-> ( x <_ y /\ y <_ x ) ) )
11	10	biimprd	|- ( ( x e. RR* /\ y e. RR* ) -> ( ( x <_ y /\ y <_ x ) -> x = y ) )
12	7 9 11	syl2an	|- ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( ( x <_ y /\ y <_ x ) -> x = y ) )
13		eliccxr	|- ( z e. ( 0 [,] +oo ) -> z e. RR* )
14		xrletr	|- ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( x <_ y /\ y <_ z ) -> x <_ z ) )
15	7 9 13 14	syl3an	|- ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) /\ z e. ( 0 [,] +oo ) ) -> ( ( x <_ y /\ y <_ z ) -> x <_ z ) )
16	4 5 6 8 12 15	isposi	|- ( RR*s |`s ( 0 [,] +oo ) ) e. Poset
17		xrletri	|- ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y \/ y <_ x ) )
18	7 9 17	syl2an	|- ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) -> ( x <_ y \/ y <_ x ) )
19	18	rgen2	|- A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( x <_ y \/ y <_ x )
20	5 6	istos	|- ( ( RR*s |`s ( 0 [,] +oo ) ) e. Toset <-> ( ( RR*s |`s ( 0 [,] +oo ) ) e. Poset /\ A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) ( x <_ y \/ y <_ x ) ) )
21	16 19 20	mpbir2an	|- ( RR*s |`s ( 0 [,] +oo ) ) e. Toset
22		xleadd1a	|- ( ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) /\ x <_ y ) -> ( x +e z ) <_ ( y +e z ) )
23	22	ex	|- ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( x <_ y -> ( x +e z ) <_ ( y +e z ) ) )
24	7 9 13 23	syl3an	|- ( ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) /\ z e. ( 0 [,] +oo ) ) -> ( x <_ y -> ( x +e z ) <_ ( y +e z ) ) )
25	24	rgen3	|- A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) A. z e. ( 0 [,] +oo ) ( x <_ y -> ( x +e z ) <_ ( y +e z ) )
26		xrge0plusg	|- +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
27	5 26 6	isomnd	|- ( ( RR*s |`s ( 0 [,] +oo ) ) e. oMnd <-> ( ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. Toset /\ A. x e. ( 0 [,] +oo ) A. y e. ( 0 [,] +oo ) A. z e. ( 0 [,] +oo ) ( x <_ y -> ( x +e z ) <_ ( y +e z ) ) ) )
28	3 21 25 27	mpbir3an	|- ( RR*s |`s ( 0 [,] +oo ) ) e. oMnd