Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-com1 Unicode version

Definition df-com1 25435
Description: A device to add commutativity to magmas, semi-groups, monoids and so on. A commutative group is composed of 5 properties (internal operation, commutativity, associativity, existence of a neutral element and an inverse). If we switch on or off those four properties we get 32 structures. Instead of giving a name to those 32 structures, I suggest we use intersected classes and speak of  (
Magma  i^i  Com1 ) or  ( Magma  i^i  ExId  ). (Contributed by FL, 5-Sep-2010.)
Assertion
Ref Expression
df-com1  |-  Com1  =  { g  |  A. x  e.  dom  dom  g A. y  e.  dom  dom  g ( x g y )  =  ( y g x ) }
Distinct variable group:    x, g, y

Detailed syntax breakdown of Definition df-com1
StepHypRef Expression
1 ccm1 25434 . 2  class  Com1
2 vx . . . . . . . 8  set  x
32cv 1631 . . . . . . 7  class  x
4 vy . . . . . . . 8  set  y
54cv 1631 . . . . . . 7  class  y
6 vg . . . . . . . 8  set  g
76cv 1631 . . . . . . 7  class  g
83, 5, 7co 5874 . . . . . 6  class  ( x g y )
95, 3, 7co 5874 . . . . . 6  class  ( y g x )
108, 9wceq 1632 . . . . 5  wff  ( x g y )  =  ( y g x )
117cdm 4705 . . . . . 6  class  dom  g
1211cdm 4705 . . . . 5  class  dom  dom  g
1310, 4, 12wral 2556 . . . 4  wff  A. y  e.  dom  dom  g (
x g y )  =  ( y g x )
1413, 2, 12wral 2556 . . 3  wff  A. x  e.  dom  dom  g A. y  e.  dom  dom  g
( x g y )  =  ( y g x )
1514, 6cab 2282 . 2  class  { g  |  A. x  e. 
dom  dom  g A. y  e.  dom  dom  g (
x g y )  =  ( y g x ) }
161, 15wceq 1632 1  wff  Com1  =  { g  |  A. x  e.  dom  dom  g A. y  e.  dom  dom  g ( x g y )  =  ( y g x ) }
Colors of variables: wff set class
This definition is referenced by:  iscom  25436
  Copyright terms: Public domain W3C validator