Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-omnd Structured version   Unicode version

Definition df-omnd 27339
 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 oppg. (Contributed by Thierry Arnoux, 13-Mar-2018.)
Assertion
Ref Expression
df-omnd oMnd Toset
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-omnd
StepHypRef Expression
1 comnd 27337 . 2 oMnd
2 vg . . . . . . . . 9
32cv 1373 . . . . . . . 8
4 ctos 15511 . . . . . . . 8 Toset
53, 4wcel 1762 . . . . . . 7 Toset
6 va . . . . . . . . . . . . 13
76cv 1373 . . . . . . . . . . . 12
8 vb . . . . . . . . . . . . 13
98cv 1373 . . . . . . . . . . . 12
10 vl . . . . . . . . . . . . 13
1110cv 1373 . . . . . . . . . . . 12
127, 9, 11wbr 4442 . . . . . . . . . . 11
13 vc . . . . . . . . . . . . . 14
1413cv 1373 . . . . . . . . . . . . 13
15 vp . . . . . . . . . . . . . 14
1615cv 1373 . . . . . . . . . . . . 13
177, 14, 16co 6277 . . . . . . . . . . . 12
189, 14, 16co 6277 . . . . . . . . . . . 12
1917, 18, 11wbr 4442 . . . . . . . . . . 11
2012, 19wi 4 . . . . . . . . . 10
21 vv . . . . . . . . . . 11
2221cv 1373 . . . . . . . . . 10
2320, 13, 22wral 2809 . . . . . . . . 9
2423, 8, 22wral 2809 . . . . . . . 8
2524, 6, 22wral 2809 . . . . . . 7
265, 25wa 369 . . . . . 6 Toset
27 cple 14553 . . . . . . 7
283, 27cfv 5581 . . . . . 6
2926, 10, 28wsbc 3326 . . . . 5 Toset
30 cplusg 14546 . . . . . 6
313, 30cfv 5581 . . . . 5
3229, 15, 31wsbc 3326 . . . 4 Toset
33 cbs 14481 . . . . 5
343, 33cfv 5581 . . . 4
3532, 21, 34wsbc 3326 . . 3 Toset
36 cmnd 15717 . . 3
3735, 2, 36crab 2813 . 2 Toset
381, 37wceq 1374 1 oMnd Toset
 Colors of variables: wff setvar class This definition is referenced by:  isomnd  27341
 Copyright terms: Public domain W3C validator