Definition df-cmn 12886

Description: Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)

Assertion

Ref	Expression
df-cmn	⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}

Distinct variable group:   𝑎,𝑏,𝑔

Detailed syntax breakdown of Definition df-cmn

Step	Hyp	Ref	Expression
1		ccmn 12884	. 2 class CMnd
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1352	. . . . . . 7 class 𝑎
4		vb	. . . . . . . 8 setvar 𝑏
5	4	cv 1352	. . . . . . 7 class 𝑏
6		vg	. . . . . . . . 9 setvar 𝑔
7	6	cv 1352	. . . . . . . 8 class 𝑔
8		cplusg 12492	. . . . . . . 8 class +g
9	7, 8	cfv 5208	. . . . . . 7 class (+g‘𝑔)
10	3, 5, 9	co 5865	. . . . . 6 class (𝑎(+g‘𝑔)𝑏)
11	5, 3, 9	co 5865	. . . . . 6 class (𝑏(+g‘𝑔)𝑎)
12	10, 11	wceq 1353	. . . . 5 wff (𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)
13		cbs 12428	. . . . . 6 class Base
14	7, 13	cfv 5208	. . . . 5 class (Base‘𝑔)
15	12, 4, 14	wral 2453	. . . 4 wff ∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)
16	15, 2, 14	wral 2453	. . 3 wff ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)
17		cmnd 12682	. . 3 class Mnd
18	16, 6, 17	crab 2457	. 2 class {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}
19	1, 18	wceq 1353	1 wff CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}

This definition is referenced by:  iscmn  12892