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

Definition df-cmn 15091
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 15089 . 2  class CMnd
2 va . . . . . . . 8  set  a
32cv 1622 . . . . . . 7  class  a
4 vb . . . . . . . 8  set  b
54cv 1622 . . . . . . 7  class  b
6 vg . . . . . . . . 9  set  g
76cv 1622 . . . . . . . 8  class  g
8 cplusg 13208 . . . . . . . 8  class  +g
97, 8cfv 5255 . . . . . . 7  class  ( +g  `  g )
103, 5, 9co 5858 . . . . . 6  class  ( a ( +g  `  g
) b )
115, 3, 9co 5858 . . . . . 6  class  ( b ( +g  `  g
) a )
1210, 11wceq 1623 . . . . 5  wff  ( a ( +g  `  g
) b )  =  ( b ( +g  `  g ) a )
13 cbs 13148 . . . . . 6  class  Base
147, 13cfv 5255 . . . . 5  class  ( Base `  g )
1512, 4, 14wral 2543 . . . 4  wff  A. b  e.  ( Base `  g
) ( a ( +g  `  g ) b )  =  ( b ( +g  `  g
) a )
1615, 2, 14wral 2543 . . 3  wff  A. a  e.  ( Base `  g
) A. b  e.  ( Base `  g
) ( a ( +g  `  g ) b )  =  ( b ( +g  `  g
) a )
17 cmnd 14361 . . 3  class  Mnd
1816, 6, 17crab 2547 . 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 1623 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  15096
  Copyright terms: Public domain W3C validator