Definition df-ass 10360

Description: A device to add associativity to various sorts of internal operations. The definition is meaningful when g is a magma at least.

Assertion

Ref	Expression
df-ass	|- Ass = {g | A.x e. dom dom gA.y e. dom dom gA.z e. dom dom g((xgy)gz) = (xg(ygz))}

Distinct variable group:   x,g,y,z

Detailed syntax breakdown of Definition df-ass

Step	Hyp	Ref	Expression
1		cass 10359	. 2 class Ass
2		vx	. . . . . . . . . 10 set x
3	2	cv 1297	. . . . . . . . 9 class x
4		vy	. . . . . . . . . 10 set y
5	4	cv 1297	. . . . . . . . 9 class y
6		vg	. . . . . . . . . 10 set g
7	6	cv 1297	. . . . . . . . 9 class g
8	3, 5, 7	co 4884	. . . . . . . 8 class (xgy)
9		vz	. . . . . . . . 9 set z
10	9	cv 1297	. . . . . . . 8 class z
11	8, 10, 7	co 4884	. . . . . . 7 class ((xgy)gz)
12	5, 10, 7	co 4884	. . . . . . . 8 class (ygz)
13	3, 12, 7	co 4884	. . . . . . 7 class (xg(ygz))
14	11, 13	wceq 1298	. . . . . 6 wff ((xgy)gz) = (xg(ygz))
15	7	cdm 3986	. . . . . . 7 class dom g
16	15	cdm 3986	. . . . . 6 class dom dom g
17	14, 9, 16	wral 2105	. . . . 5 wff A.z e. dom dom g((xgy)gz) = (xg(ygz))
18	17, 4, 16	wral 2105	. . . 4 wff A.y e. dom dom gA.z e. dom dom g((xgy)gz) = (xg(ygz))
19	18, 2, 16	wral 2105	. . 3 wff A.x e. dom dom gA.y e. dom dom gA.z e. dom dom g((xgy)gz) = (xg(ygz))
20	19, 6	cab 1871	. 2 class {g | A.x e. dom dom gA.y e. dom dom gA.z e. dom dom g((xgy)gz) = (xg(ygz))}
21	1, 20	wceq 1298	1 wff Ass = {g | A.x e. dom dom gA.y e. dom dom gA.z e. dom dom g((xgy)gz) = (xg(ygz))}

This definition is referenced by:  isass 10363

Copyright terms: Public domain