# 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}\mathrm{oMnd}$
1 vg ${setvar}{g}$
2 cmnd ${class}\mathrm{Mnd}$
3 cbs ${class}\mathrm{Base}$
4 1 cv ${setvar}{g}$
5 4 3 cfv ${class}{\mathrm{Base}}_{{g}}$
6 vv ${setvar}{v}$
7 cplusg ${class}{+}_{𝑔}$
8 4 7 cfv ${class}{+}_{{g}}$
9 vp ${setvar}{p}$
10 cple ${class}\mathrm{le}$
11 4 10 cfv ${class}{\le }_{{g}}$
12 vl ${setvar}{l}$
13 ctos ${class}\mathrm{Toset}$
14 4 13 wcel ${wff}{g}\in \mathrm{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}\left({a}{p}{c}\right)$
26 21 24 23 co ${class}\left({b}{p}{c}\right)$
27 25 26 20 wbr ${wff}\left({a}{p}{c}\right){l}\left({b}{p}{c}\right)$
28 22 27 wi ${wff}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)$
29 28 18 16 wral ${wff}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)$
30 29 17 16 wral ${wff}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)$
31 30 15 16 wral ${wff}\forall {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)$
32 14 31 wa ${wff}\left({g}\in \mathrm{Toset}\wedge \forall {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)\right)$
33 32 12 11 wsbc
34 33 9 8 wsbc
35 34 6 5 wsbc
36 35 1 2 crab
37 0 36 wceq