This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ass

Description: A device to add associativity to various sorts of internal operations. The definition is meaningful when g is a magma at least. (Contributed by FL, 1-Nov-2009) (New usage is discouraged.)

Ref Expression
Assertion df-ass 
|- Ass = { g | A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cass 
 |-  Ass
1 vg 
 |-  g
2 vx 
 |-  x
3 1 cv 
 |-  g
4 3 cdm 
 |-  dom g
5 4 cdm 
 |-  dom dom g
6 vy 
 |-  y
7 vz 
 |-  z
8 2 cv 
 |-  x
9 6 cv 
 |-  y
10 8 9 3 co 
 |-  ( x g y )
11 7 cv 
 |-  z
12 10 11 3 co 
 |-  ( ( x g y ) g z )
13 9 11 3 co 
 |-  ( y g z )
14 8 13 3 co 
 |-  ( x g ( y g z ) )
15 12 14 wceq 
 |-  ( ( x g y ) g z ) = ( x g ( y g z ) )
16 15 7 5 wral 
 |-  A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) )
17 16 6 5 wral 
 |-  A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) )
18 17 2 5 wral 
 |-  A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) )
19 18 1 cab 
 |-  { g | A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) }
20 0 19 wceq 
 |-  Ass = { g | A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) }