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

Metamath Proof Explorer

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