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 ∈ Mnd | [˙Base g / v]˙ [˙+ g / p]˙ [˙≤ g / l]˙ g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c

Detailed syntax breakdown

Step Hyp Ref Expression
0 comnd class oMnd
1 vg setvar g
2 cmnd class Mnd
3 cbs class Base
4 1 cv setvar g
5 4 3 cfv class Base g
6 vv setvar v
7 cplusg class + 𝑔
8 4 7 cfv class + g
9 vp setvar p
10 cple class le
11 4 10 cfv class ≤ g
12 vl setvar l
13 ctos class Toset
14 4 13 wcel wff g ∈ Toset
15 va setvar a
16 6 cv setvar v
17 vb setvar b
18 vc setvar c
19 15 cv setvar a
20 12 cv setvar l
21 17 cv setvar b
22 19 21 20 wbr wff a l b
23 9 cv setvar p
24 18 cv setvar c
25 19 24 23 co class a p c
26 21 24 23 co class b p c
27 25 26 20 wbr wff a p c l b p c
28 22 27 wi wff a l b → a p c l b p c
29 28 18 16 wral wff ∀ c ∈ v a l b → a p c l b p c
30 29 17 16 wral wff ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
31 30 15 16 wral wff ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
32 14 31 wa wff g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
33 32 12 11 wsbc wff [˙≤ g / l]˙ g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
34 33 9 8 wsbc wff [˙+ g / p]˙ [˙≤ g / l]˙ g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
35 34 6 5 wsbc wff [˙Base g / v]˙ [˙+ g / p]˙ [˙≤ g / l]˙ g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
36 35 1 2 crab class g ∈ Mnd | [˙Base g / v]˙ [˙+ g / p]˙ [˙≤ g / l]˙ g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c
37 0 36 wceq wff oMnd = g ∈ Mnd | [˙Base g / v]˙ [˙+ g / p]˙ [˙≤ g / l]˙ g ∈ Toset ∧ ∀ a ∈ v ∀ b ∈ v ∀ c ∈ v a l b → a p c l b p c