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 ) ) }