Definition df-omnd 29699

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 (opp_g ` 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

Step	Hyp	Ref	Expression
1		comnd 29697	. 2 class oMnd
2		vg	. . . . . . . . 9 setvar g
3	2	cv 1482	. . . . . . . 8 class g
4		ctos 17033	. . . . . . . 8 class Toset
5	3, 4	wcel 1990	. . . . . . 7 wff g e. Toset
6		va	. . . . . . . . . . . . 13 setvar a
7	6	cv 1482	. . . . . . . . . . . 12 class a
8		vb	. . . . . . . . . . . . 13 setvar b
9	8	cv 1482	. . . . . . . . . . . 12 class b
10		vl	. . . . . . . . . . . . 13 setvar l
11	10	cv 1482	. . . . . . . . . . . 12 class l
12	7, 9, 11	wbr 4653	. . . . . . . . . . 11 wff a l b
13		vc	. . . . . . . . . . . . . 14 setvar c
14	13	cv 1482	. . . . . . . . . . . . 13 class c
15		vp	. . . . . . . . . . . . . 14 setvar p
16	15	cv 1482	. . . . . . . . . . . . 13 class p
17	7, 14, 16	co 6650	. . . . . . . . . . . 12 class ( a p c )
18	9, 14, 16	co 6650	. . . . . . . . . . . 12 class ( b p c )
19	17, 18, 11	wbr 4653	. . . . . . . . . . 11 wff ( a p c ) l ( b p c )
20	12, 19	wi 4	. . . . . . . . . 10 wff ( a l b -> ( a p c ) l ( b p c ) )
21		vv	. . . . . . . . . . 11 setvar v
22	21	cv 1482	. . . . . . . . . 10 class v
23	20, 13, 22	wral 2912	. . . . . . . . 9 wff A. c e. v ( a l b -> ( a p c ) l ( b p c ) )
24	23, 8, 22	wral 2912	. . . . . . . 8 wff A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) )
25	24, 6, 22	wral 2912	. . . . . . 7 wff A. a e. v A. b e. v A. c e. v ( a l b -> ( a p c ) l ( b p c ) )
26	5, 25	wa 384	. . . . . 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 15948	. . . . . . 7 class le
28	3, 27	cfv 5888	. . . . . 6 class ( le ` g )
29	26, 10, 28	wsbc 3435	. . . . 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 15941	. . . . . 6 class +g
31	3, 30	cfv 5888	. . . . 5 class ( +g ` g )
32	29, 15, 31	wsbc 3435	. . . 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 15857	. . . . 5 class Base
34	3, 33	cfv 5888	. . . 4 class ( Base ` g )
35	32, 21, 34	wsbc 3435	. . 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 17294	. . 3 class Mnd
37	35, 2, 36	crab 2916	. 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 ) ) ) }
38	1, 37	wceq 1483	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 ) ) ) }

This definition is referenced by:  isomnd  29701