MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cmn Unicode version

Definition df-cmn 15402
Description: Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
df-cmn  |- CMnd  =  {
g  e.  Mnd  |  A. a  e.  ( Base `  g ) A. b  e.  ( Base `  g ) ( a ( +g  `  g
) b )  =  ( b ( +g  `  g ) a ) }
Distinct variable group:    a, b, g

Detailed syntax breakdown of Definition df-cmn
StepHypRef Expression
1 ccmn 15400 . 2  class CMnd
2 va . . . . . . . 8  set  a
32cv 1651 . . . . . . 7  class  a
4 vb . . . . . . . 8  set  b
54cv 1651 . . . . . . 7  class  b
6 vg . . . . . . . . 9  set  g
76cv 1651 . . . . . . . 8  class  g
8 cplusg 13517 . . . . . . . 8  class  +g
97, 8cfv 5445 . . . . . . 7  class  ( +g  `  g )
103, 5, 9co 6072 . . . . . 6  class  ( a ( +g  `  g
) b )
115, 3, 9co 6072 . . . . . 6  class  ( b ( +g  `  g
) a )
1210, 11wceq 1652 . . . . 5  wff  ( a ( +g  `  g
) b )  =  ( b ( +g  `  g ) a )
13 cbs 13457 . . . . . 6  class  Base
147, 13cfv 5445 . . . . 5  class  ( Base `  g )
1512, 4, 14wral 2697 . . . 4  wff  A. b  e.  ( Base `  g
) ( a ( +g  `  g ) b )  =  ( b ( +g  `  g
) a )
1615, 2, 14wral 2697 . . 3  wff  A. a  e.  ( Base `  g
) A. b  e.  ( Base `  g
) ( a ( +g  `  g ) b )  =  ( b ( +g  `  g
) a )
17 cmnd 14672 . . 3  class  Mnd
1816, 6, 17crab 2701 . 2  class  { g  e.  Mnd  |  A. a  e.  ( Base `  g ) A. b  e.  ( Base `  g
) ( a ( +g  `  g ) b )  =  ( b ( +g  `  g
) a ) }
191, 18wceq 1652 1  wff CMnd  =  {
g  e.  Mnd  |  A. a  e.  ( Base `  g ) A. b  e.  ( Base `  g ) ( a ( +g  `  g
) b )  =  ( b ( +g  `  g ) a ) }
Colors of variables: wff set class
This definition is referenced by:  iscmn  15407
  Copyright terms: Public domain W3C validator