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∈Mnd|[˙Baseg/v]˙[˙+g/p]˙[˙≤g/l]˙g∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc

Detailed syntax breakdown

Step Hyp Ref Expression
0 comnd classoMnd
1 vg setvarg
2 cmnd classMnd
3 cbs classBase
4 1 cv setvarg
5 4 3 cfv classBaseg
6 vv setvarv
7 cplusg class+𝑔
8 4 7 cfv class+g
9 vp setvarp
10 cple classle
11 4 10 cfv class≤g
12 vl setvarl
13 ctos classToset
14 4 13 wcel wffg∈Toset
15 va setvara
16 6 cv setvarv
17 vb setvarb
18 vc setvarc
19 15 cv setvara
20 12 cv setvarl
21 17 cv setvarb
22 19 21 20 wbr wffalb
23 9 cv setvarp
24 18 cv setvarc
25 19 24 23 co classapc
26 21 24 23 co classbpc
27 25 26 20 wbr wffapclbpc
28 22 27 wi wffalb→apclbpc
29 28 18 16 wral wff∀c∈valb→apclbpc
30 29 17 16 wral wff∀b∈v∀c∈valb→apclbpc
31 30 15 16 wral wff∀a∈v∀b∈v∀c∈valb→apclbpc
32 14 31 wa wffg∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc
33 32 12 11 wsbc wff[˙≤g/l]˙g∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc
34 33 9 8 wsbc wff[˙+g/p]˙[˙≤g/l]˙g∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc
35 34 6 5 wsbc wff[˙Baseg/v]˙[˙+g/p]˙[˙≤g/l]˙g∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc
36 35 1 2 crab classg∈Mnd|[˙Baseg/v]˙[˙+g/p]˙[˙≤g/l]˙g∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc
37 0 36 wceq wffoMnd=g∈Mnd|[˙Baseg/v]˙[˙+g/p]˙[˙≤g/l]˙g∈Toset∧∀a∈v∀b∈v∀c∈valb→apclbpc