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 = { 𝑔 ∈ Mnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] [ ( le ‘ 𝑔 ) / 𝑙 ] ( 𝑔 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		comnd	⊢ oMnd
1		vg	⊢ 𝑔
2		cmnd	⊢ Mnd
3		cbs	⊢ Base
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( Base ‘ 𝑔 )
6		vv	⊢ 𝑣
7		cplusg	⊢ +g
8	4 7	cfv	⊢ ( +g ‘ 𝑔 )
9		vp	⊢ 𝑝
10		cple	⊢ le
11	4 10	cfv	⊢ ( le ‘ 𝑔 )
12		vl	⊢ 𝑙
13		ctos	⊢ Toset
14	4 13	wcel	⊢ 𝑔 ∈ Toset
15		va	⊢ 𝑎
16	6	cv	⊢ 𝑣
17		vb	⊢ 𝑏
18		vc	⊢ 𝑐
19	15	cv	⊢ 𝑎
20	12	cv	⊢ 𝑙
21	17	cv	⊢ 𝑏
22	19 21 20	wbr	⊢ 𝑎 𝑙 𝑏
23	9	cv	⊢ 𝑝
24	18	cv	⊢ 𝑐
25	19 24 23	co	⊢ ( 𝑎 𝑝 𝑐 )
26	21 24 23	co	⊢ ( 𝑏 𝑝 𝑐 )
27	25 26 20	wbr	⊢ ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 )
28	22 27	wi	⊢ ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) )
29	28 18 16	wral	⊢ ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) )
30	29 17 16	wral	⊢ ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) )
31	30 15 16	wral	⊢ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) )
32	14 31	wa	⊢ ( 𝑔 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) )
33	32 12 11	wsbc	⊢ [ ( le ‘ 𝑔 ) / 𝑙 ] ( 𝑔 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) )
34	33 9 8	wsbc	⊢ [ ( +g ‘ 𝑔 ) / 𝑝 ] [ ( le ‘ 𝑔 ) / 𝑙 ] ( 𝑔 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) )
35	34 6 5	wsbc	⊢ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] [ ( le ‘ 𝑔 ) / 𝑙 ] ( 𝑔 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) )
36	35 1 2	crab	⊢ { 𝑔 ∈ Mnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] [ ( le ‘ 𝑔 ) / 𝑙 ] ( 𝑔 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) }
37	0 36	wceq	⊢ oMnd = { 𝑔 ∈ Mnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] [ ( le ‘ 𝑔 ) / 𝑙 ] ( 𝑔 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) }