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

Definition df-omnd 28832
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 = {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))}
Distinct variable group:   𝑎,𝑏,𝑐,𝑔,𝑙,𝑝,𝑣

Detailed syntax breakdown of Definition df-omnd
StepHypRef Expression
1 comnd 28830 . 2 class oMnd
2 vg . . . . . . . . 9 setvar 𝑔
32cv 1473 . . . . . . . 8 class 𝑔
4 ctos 16798 . . . . . . . 8 class Toset
53, 4wcel 1975 . . . . . . 7 wff 𝑔 ∈ Toset
6 va . . . . . . . . . . . . 13 setvar 𝑎
76cv 1473 . . . . . . . . . . . 12 class 𝑎
8 vb . . . . . . . . . . . . 13 setvar 𝑏
98cv 1473 . . . . . . . . . . . 12 class 𝑏
10 vl . . . . . . . . . . . . 13 setvar 𝑙
1110cv 1473 . . . . . . . . . . . 12 class 𝑙
127, 9, 11wbr 4573 . . . . . . . . . . 11 wff 𝑎𝑙𝑏
13 vc . . . . . . . . . . . . . 14 setvar 𝑐
1413cv 1473 . . . . . . . . . . . . 13 class 𝑐
15 vp . . . . . . . . . . . . . 14 setvar 𝑝
1615cv 1473 . . . . . . . . . . . . 13 class 𝑝
177, 14, 16co 6523 . . . . . . . . . . . 12 class (𝑎𝑝𝑐)
189, 14, 16co 6523 . . . . . . . . . . . 12 class (𝑏𝑝𝑐)
1917, 18, 11wbr 4573 . . . . . . . . . . 11 wff (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)
2012, 19wi 4 . . . . . . . . . 10 wff (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
21 vv . . . . . . . . . . 11 setvar 𝑣
2221cv 1473 . . . . . . . . . 10 class 𝑣
2320, 13, 22wral 2891 . . . . . . . . 9 wff 𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
2423, 8, 22wral 2891 . . . . . . . 8 wff 𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
2524, 6, 22wral 2891 . . . . . . 7 wff 𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
265, 25wa 382 . . . . . 6 wff (𝑔 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
27 cple 15717 . . . . . . 7 class le
283, 27cfv 5786 . . . . . 6 class (le‘𝑔)
2926, 10, 28wsbc 3397 . . . . 5 wff [(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
30 cplusg 15710 . . . . . 6 class +g
313, 30cfv 5786 . . . . 5 class (+g𝑔)
3229, 15, 31wsbc 3397 . . . 4 wff [(+g𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
33 cbs 15637 . . . . 5 class Base
343, 33cfv 5786 . . . 4 class (Base‘𝑔)
3532, 21, 34wsbc 3397 . . 3 wff [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
36 cmnd 17059 . . 3 class Mnd
3735, 2, 36crab 2895 . 2 class {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))}
381, 37wceq 1474 1 wff oMnd = {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎𝑣𝑏𝑣𝑐𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))}
Colors of variables: wff setvar class
This definition is referenced by:  isomnd  28834
  Copyright terms: Public domain W3C validator