# Metamath Proof Explorer

## Definition df-omnd

Description: Define class of all right ordered monoids. An ordered monoid is a monoid with a total ordering compatible with its operation. It is possible to use this definition also for left ordered monoids, by applying it to ( oppGM ) . (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Assertion df-omnd

### Detailed syntax breakdown

Step Hyp Ref Expression
0 comnd $class oMnd$
1 vg $setvar g$
2 cmnd $class Mnd$
3 cbs $class Base$
4 1 cv $setvar g$
5 4 3 cfv $class Base g$
6 vv $setvar v$
7 cplusg $class + 𝑔$
8 4 7 cfv $class + g$
9 vp $setvar p$
10 cple $class le$
11 4 10 cfv $class ≤ g$
12 vl $setvar l$
13 ctos $class Toset$
14 4 13 wcel $wff g ∈ Toset$
15 va $setvar a$
16 6 cv $setvar v$
17 vb $setvar b$
18 vc $setvar c$
19 15 cv $setvar a$
20 12 cv $setvar l$
21 17 cv $setvar b$
22 19 21 20 wbr $wff a l b$
23 9 cv $setvar p$
24 18 cv $setvar c$
25 19 24 23 co $class a p c$
26 21 24 23 co $class b p c$
27 25 26 20 wbr $wff a p c l b p c$
28 22 27 wi $wff a l b → a p c l b p c$
29 28 18 16 wral $wff ∀ c ∈ v a l b → a p c l b p c$
30 29 17 16 wral $wff ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c$
31 30 15 16 wral $wff ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c$
32 14 31 wa $wff g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c$
33 32 12 11 wsbc
34 33 9 8 wsbc
35 34 6 5 wsbc
36 35 1 2 crab
37 0 36 wceq