Definition df-omnd 32248

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‘𝑀). (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

Step	Hyp	Ref	Expression
1		comnd 32246	. 2 class oMnd
2		vg	. . . . . . . . 9 setvar 𝑔
3	2	cv 1541	. . . . . . . 8 class 𝑔
4		ctos 18369	. . . . . . . 8 class Toset
5	3, 4	wcel 2107	. . . . . . 7 wff 𝑔 ∈ Toset
6		va	. . . . . . . . . . . . 13 setvar 𝑎
7	6	cv 1541	. . . . . . . . . . . 12 class 𝑎
8		vb	. . . . . . . . . . . . 13 setvar 𝑏
9	8	cv 1541	. . . . . . . . . . . 12 class 𝑏
10		vl	. . . . . . . . . . . . 13 setvar 𝑙
11	10	cv 1541	. . . . . . . . . . . 12 class 𝑙
12	7, 9, 11	wbr 5149	. . . . . . . . . . 11 wff 𝑎𝑙𝑏
13		vc	. . . . . . . . . . . . . 14 setvar 𝑐
14	13	cv 1541	. . . . . . . . . . . . 13 class 𝑐
15		vp	. . . . . . . . . . . . . 14 setvar 𝑝
16	15	cv 1541	. . . . . . . . . . . . 13 class 𝑝
17	7, 14, 16	co 7409	. . . . . . . . . . . 12 class (𝑎𝑝𝑐)
18	9, 14, 16	co 7409	. . . . . . . . . . . 12 class (𝑏𝑝𝑐)
19	17, 18, 11	wbr 5149	. . . . . . . . . . 11 wff (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)
20	12, 19	wi 4	. . . . . . . . . 10 wff (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
21		vv	. . . . . . . . . . 11 setvar 𝑣
22	21	cv 1541	. . . . . . . . . 10 class 𝑣
23	20, 13, 22	wral 3062	. . . . . . . . 9 wff ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
24	23, 8, 22	wral 3062	. . . . . . . 8 wff ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
25	24, 6, 22	wral 3062	. . . . . . 7 wff ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐))
26	5, 25	wa 397	. . . . . 6 wff (𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
27		cple 17204	. . . . . . 7 class le
28	3, 27	cfv 6544	. . . . . 6 class (le‘𝑔)
29	26, 10, 28	wsbc 3778	. . . . 5 wff [(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
30		cplusg 17197	. . . . . 6 class +g
31	3, 30	cfv 6544	. . . . 5 class (+g‘𝑔)
32	29, 15, 31	wsbc 3778	. . . 4 wff [(+g‘𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
33		cbs 17144	. . . . 5 class Base
34	3, 33	cfv 6544	. . . 4 class (Base‘𝑔)
35	32, 21, 34	wsbc 3778	. . 3 wff [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))
36		cmnd 18625	. . 3 class Mnd
37	35, 2, 36	crab 3433	. 2 class {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))}
38	1, 37	wceq 1542	1 wff oMnd = {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))}

This definition is referenced by:  isomnd  32250