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 26298
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 26296 . 2  class oMnd
2 vg . . . . . . . . 9  setvar  g
32cv 1369 . . . . . . . 8  class  g
4 ctos 15307 . . . . . . . 8  class Toset
53, 4wcel 1758 . . . . . . 7  wff  g  e. Toset
6 va . . . . . . . . . . . . 13  setvar  a
76cv 1369 . . . . . . . . . . . 12  class  a
8 vb . . . . . . . . . . . . 13  setvar  b
98cv 1369 . . . . . . . . . . . 12  class  b
10 vl . . . . . . . . . . . . 13  setvar  l
1110cv 1369 . . . . . . . . . . . 12  class  l
127, 9, 11wbr 4392 . . . . . . . . . . 11  wff  a l b
13 vc . . . . . . . . . . . . . 14  setvar  c
1413cv 1369 . . . . . . . . . . . . 13  class  c
15 vp . . . . . . . . . . . . . 14  setvar  p
1615cv 1369 . . . . . . . . . . . . 13  class  p
177, 14, 16co 6192 . . . . . . . . . . . 12  class  ( a p c )
189, 14, 16co 6192 . . . . . . . . . . . 12  class  ( b p c )
1917, 18, 11wbr 4392 . . . . . . . . . . 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 1369 . . . . . . . . . 10  class  v
2320, 13, 22wral 2795 . . . . . . . . 9  wff  A. c  e.  v  ( a
l b  ->  (
a p c ) l ( b p c ) )
2423, 8, 22wral 2795 . . . . . . . 8  wff  A. b  e.  v  A. c  e.  v  ( a
l b  ->  (
a p c ) l ( b p c ) )
2524, 6, 22wral 2795 . . . . . . 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 14349 . . . . . . 7  class  le
283, 27cfv 5518 . . . . . 6  class  ( le
`  g )
2926, 10, 28wsbc 3286 . . . . 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 14342 . . . . . 6  class  +g
313, 30cfv 5518 . . . . 5  class  ( +g  `  g )
3229, 15, 31wsbc 3286 . . . 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 14278 . . . . 5  class  Base
343, 33cfv 5518 . . . 4  class  ( Base `  g )
3532, 21, 34wsbc 3286 . . 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 15513 . . 3  class  Mnd
3735, 2, 36crab 2799 . 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 1370 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  26300
  Copyright terms: Public domain W3C validator