Users' Mathboxes 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
`  M ). (Contributed by Thierry Arnoux, 13-Mar-2018.)
Assertion
Ref Expression
df-omnd  |- oMnd  =  {
g  e.  Mnd  |  [. ( Base `  g
)  /  v ]. [. ( +g  `  g
)  /  p ]. [. ( le `  g
)  /  l ]. ( g  e. Toset  /\  A. a  e.  v  A. b  e.  v  A. c  e.  v  (
a l b  -> 
( a p c ) l ( b p c ) ) ) }
Distinct variable group:    a, b, c, g, l, p, v

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