Metamath Proof Explorer

Definition df-cmn

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

Ref Expression
Assertion df-cmn 
|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmn 
 |-  CMnd
1 vg 
 |-  g
2 cmnd 
 |-  Mnd
3 va 
 |-  a
4 cbs 
 |-  Base
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Base ` g )
7 vb 
 |-  b
8 3 cv 
 |-  a
9 cplusg 
 |-  +g
10 5 9 cfv 
 |-  ( +g ` g )
11 7 cv 
 |-  b
12 8 11 10 co 
 |-  ( a ( +g ` g ) b )
13 11 8 10 co 
 |-  ( b ( +g ` g ) a )
14 12 13 wceq 
 |-  ( a ( +g ` g ) b ) = ( b ( +g ` g ) a )
15 14 7 6 wral 
 |-  A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a )
16 15 3 6 wral 
 |-  A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a )
17 16 1 2 crab 
 |-  { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
18 0 17 wceq 
 |-  CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }