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