This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { 𝑔 ∈ 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 ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) }