# 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
`|- oMnd = { g e. Mnd | [. ( Base ` g ) / v ]. [. ( +g ` g ) / p ]. [. ( le ` g ) / l ]. ( g e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) }`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 comnd
` |-  oMnd`
1 vg
` |-  g`
2 cmnd
` |-  Mnd`
3 cbs
` |-  Base`
4 1 cv
` |-  g`
5 4 3 cfv
` |-  ( Base ` g )`
6 vv
` |-  v`
7 cplusg
` |-  +g`
8 4 7 cfv
` |-  ( +g ` g )`
9 vp
` |-  p`
10 cple
` |-  le`
11 4 10 cfv
` |-  ( le ` g )`
12 vl
` |-  l`
13 ctos
` |-  Toset`
14 4 13 wcel
` |-  g e. Toset`
15 va
` |-  a`
16 6 cv
` |-  v`
17 vb
` |-  b`
18 vc
` |-  c`
19 15 cv
` |-  a`
20 12 cv
` |-  l`
21 17 cv
` |-  b`
22 19 21 20 wbr
` |-  a l b`
23 9 cv
` |-  p`
24 18 cv
` |-  c`
25 19 24 23 co
` |-  ( a p c )`
26 21 24 23 co
` |-  ( b p c )`
27 25 26 20 wbr
` |-  ( a p c ) l ( b p c )`
28 22 27 wi
` |-  ( a l b -> ( a p c ) l ( b p c ) )`
29 28 18 16 wral
` |-  A. c e. v ( a l b -> ( a p c ) l ( b p c ) )`
30 29 17 16 wral
` |-  A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) )`
31 30 15 16 wral
` |-  A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) )`
32 14 31 wa
` |-  ( g e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) )`
33 32 12 11 wsbc
` |-  [. ( le ` g ) / l ]. ( g e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) )`
34 33 9 8 wsbc
` |-  [. ( +g ` g ) / p ]. [. ( le ` g ) / l ]. ( g e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) )`
35 34 6 5 wsbc
` |-  [. ( Base ` g ) / v ]. [. ( +g ` g ) / p ]. [. ( le ` g ) / l ]. ( g e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) )`
36 35 1 2 crab
` |-  { g e. Mnd | [. ( Base ` g ) / v ]. [. ( +g ` g ) / p ]. [. ( le ` g ) / l ]. ( g e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) }`
37 0 36 wceq
` |-  oMnd = { g e. Mnd | [. ( Base ` g ) / v ]. [. ( +g ` g ) / p ]. [. ( le ` g ) / l ]. ( g e. Toset /\ A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) ) ) }`