Metamath Proof Explorer

Definition df-omnd

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 ( oppGM ) . (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 comnd 
 |-  oMnd
1 vg 
 |-  g
2 cmnd 
 |-  Mnd
3 cbs 
 |-  Base
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Base ` g )
6 vv 
 |-  v
7 cplusg 
 |-  +g
8 4 7 cfv 
 |-  ( +g ` g )
9 vp 
 |-  p
10 cple 
 |-  le
11 4 10 cfv 
 |-  ( le ` g )
12 vl 
 |-  l
13 ctos 
 |-  Toset
14 4 13 wcel 
 |-  g e. Toset
15 va 
 |-  a
16 6 cv 
 |-  v
17 vb 
 |-  b
18 vc 
 |-  c
19 15 cv 
 |-  a
20 12 cv 
 |-  l
21 17 cv 
 |-  b
22 19 21 20 wbr 
 |-  a l b
23 9 cv 
 |-  p
24 18 cv 
 |-  c
25 19 24 23 co 
 |-  ( a p c )
26 21 24 23 co 
 |-  ( b p c )
27 25 26 20 wbr 
 |-  ( a p c ) l ( b p c )
28 22 27 wi 
 |-  ( a l b -> ( a p c ) l ( b p c ) )
29 28 18 16 wral 
 |-  A. c e. v ( a l b -> ( a p c ) l ( b p c ) )
30 29 17 16 wral 
 |-  A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) )
31 30 15 16 wral 
 |-  A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) )
32 14 31 wa 
 |-  ( 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 32 12 11 wsbc 
 |-  [. ( 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 ) ) )
34 33 9 8 wsbc 
 |-  [. ( +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 ) ) )
35 34 6 5 wsbc 
 |-  [. ( 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 35 1 2 crab 
 |-  { 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 ) ) ) }
37 0 36 wceq 
 |-  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 ) ) ) }