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 32212
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 32210 . 2 class oMnd
2 vg . . . . . . . . 9 setvar 𝑔
32cv 1540 . . . . . . . 8 class 𝑔
4 ctos 18368 . . . . . . . 8 class Toset
53, 4wcel 2106 . . . . . . 7 wff 𝑔 ∈ Toset
6 va . . . . . . . . . . . . 13 setvar π‘Ž
76cv 1540 . . . . . . . . . . . 12 class π‘Ž
8 vb . . . . . . . . . . . . 13 setvar 𝑏
98cv 1540 . . . . . . . . . . . 12 class 𝑏
10 vl . . . . . . . . . . . . 13 setvar 𝑙
1110cv 1540 . . . . . . . . . . . 12 class 𝑙
127, 9, 11wbr 5148 . . . . . . . . . . 11 wff π‘Žπ‘™π‘
13 vc . . . . . . . . . . . . . 14 setvar 𝑐
1413cv 1540 . . . . . . . . . . . . 13 class 𝑐
15 vp . . . . . . . . . . . . . 14 setvar 𝑝
1615cv 1540 . . . . . . . . . . . . 13 class 𝑝
177, 14, 16co 7408 . . . . . . . . . . . 12 class (π‘Žπ‘π‘)
189, 14, 16co 7408 . . . . . . . . . . . 12 class (𝑏𝑝𝑐)
1917, 18, 11wbr 5148 . . . . . . . . . . 11 wff (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)
2012, 19wi 4 . . . . . . . . . 10 wff (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))
21 vv . . . . . . . . . . 11 setvar 𝑣
2221cv 1540 . . . . . . . . . 10 class 𝑣
2320, 13, 22wral 3061 . . . . . . . . 9 wff βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))
2423, 8, 22wral 3061 . . . . . . . 8 wff βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))
2524, 6, 22wral 3061 . . . . . . 7 wff βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐))
265, 25wa 396 . . . . . 6 wff (𝑔 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))
27 cple 17203 . . . . . . 7 class le
283, 27cfv 6543 . . . . . 6 class (leβ€˜π‘”)
2926, 10, 28wsbc 3777 . . . . 5 wff [(leβ€˜π‘”) / 𝑙](𝑔 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))
30 cplusg 17196 . . . . . 6 class +g
313, 30cfv 6543 . . . . 5 class (+gβ€˜π‘”)
3229, 15, 31wsbc 3777 . . . 4 wff [(+gβ€˜π‘”) / 𝑝][(leβ€˜π‘”) / 𝑙](𝑔 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))
33 cbs 17143 . . . . 5 class Base
343, 33cfv 6543 . . . 4 class (Baseβ€˜π‘”)
3532, 21, 34wsbc 3777 . . 3 wff [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / 𝑝][(leβ€˜π‘”) / 𝑙](𝑔 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))
36 cmnd 18624 . . 3 class Mnd
3735, 2, 36crab 3432 . 2 class {𝑔 ∈ Mnd ∣ [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / 𝑝][(leβ€˜π‘”) / 𝑙](𝑔 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))}
381, 37wceq 1541 1 wff oMnd = {𝑔 ∈ Mnd ∣ [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / 𝑝][(leβ€˜π‘”) / 𝑙](𝑔 ∈ Toset ∧ βˆ€π‘Ž ∈ 𝑣 βˆ€π‘ ∈ 𝑣 βˆ€π‘ ∈ 𝑣 (π‘Žπ‘™π‘ β†’ (π‘Žπ‘π‘)𝑙(𝑏𝑝𝑐)))}
Colors of variables: wff setvar class
This definition is referenced by:  isomnd  32214
  Copyright terms: Public domain W3C validator