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 ⊢ℝ𝑠*↾𝑠0+∞∈oMnd

Proof

Step Hyp Ref Expression
1 xrge0cmn ⊢ℝ𝑠*↾𝑠0+∞∈CMnd
2 cmnmnd ⊢ℝ𝑠*↾𝑠0+∞∈CMnd→ℝ𝑠*↾𝑠0+∞∈Mnd
3 1 2 ax-mp ⊢ℝ𝑠*↾𝑠0+∞∈Mnd
4 ovex ⊢ℝ𝑠*↾𝑠0+∞∈V
5 xrge0base ⊢0+∞=Baseℝ𝑠*↾𝑠0+∞
6 xrge0le ⊢≤=≤ℝ𝑠*↾𝑠0+∞
7 eliccxr ⊢x∈0+∞→x∈ℝ*
8 7 xrleidd ⊢x∈0+∞→x≤x
9 eliccxr ⊢y∈0+∞→y∈ℝ*
10 xrletri3 ⊢x∈ℝ*∧y∈ℝ*→x=y↔x≤y∧y≤x
11 10 biimprd ⊢x∈ℝ*∧y∈ℝ*→x≤y∧y≤x→x=y
12 7 9 11 syl2an ⊢x∈0+∞∧y∈0+∞→x≤y∧y≤x→x=y
13 eliccxr ⊢z∈0+∞→z∈ℝ*
14 xrletr ⊢x∈ℝ*∧y∈ℝ*∧z∈ℝ*→x≤y∧y≤z→x≤z
15 7 9 13 14 syl3an ⊢x∈0+∞∧y∈0+∞∧z∈0+∞→x≤y∧y≤z→x≤z
16 4 5 6 8 12 15 isposi ⊢ℝ𝑠*↾𝑠0+∞∈Poset
17 xrletri ⊢x∈ℝ*∧y∈ℝ*→x≤y∨y≤x
18 7 9 17 syl2an ⊢x∈0+∞∧y∈0+∞→x≤y∨y≤x
19 18 rgen2 ⊢∀x∈0+∞∀y∈0+∞x≤y∨y≤x
20 5 6 istos ⊢ℝ𝑠*↾𝑠0+∞∈Toset↔ℝ𝑠*↾𝑠0+∞∈Poset∧∀x∈0+∞∀y∈0+∞x≤y∨y≤x
21 16 19 20 mpbir2an ⊢ℝ𝑠*↾𝑠0+∞∈Toset
22 xleadd1a ⊢x∈ℝ*∧y∈ℝ*∧z∈ℝ*∧x≤y→x+𝑒z≤y+𝑒z
23 22 ex ⊢x∈ℝ*∧y∈ℝ*∧z∈ℝ*→x≤y→x+𝑒z≤y+𝑒z
24 7 9 13 23 syl3an ⊢x∈0+∞∧y∈0+∞∧z∈0+∞→x≤y→x+𝑒z≤y+𝑒z
25 24 rgen3 ⊢∀x∈0+∞∀y∈0+∞∀z∈0+∞x≤y→x+𝑒z≤y+𝑒z
26 xrge0plusg ⊢+𝑒=+ℝ𝑠*↾𝑠0+∞
27 5 26 6 isomnd ⊢ℝ𝑠*↾𝑠0+∞∈oMnd↔ℝ𝑠*↾𝑠0+∞∈Mnd∧ℝ𝑠*↾𝑠0+∞∈Toset∧∀x∈0+∞∀y∈0+∞∀z∈0+∞x≤y→x+𝑒z≤y+𝑒z
28 3 21 25 27 mpbir3an ⊢ℝ𝑠*↾𝑠0+∞∈oMnd