Definition df-grp 9316

Description: Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54.

Assertion

Ref	Expression
df-grp	|- Grp = {g | E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))}

Distinct variable group:   t,g,u,x,y,z

Detailed syntax breakdown of Definition df-grp

Step	Hyp	Ref	Expression
1		cgr 9311	. 2 class Grp
2		vt	. . . . . . . 8 set t
3	2	cv 1297	. . . . . . 7 class t
4	3, 3	cxp 3984	. . . . . 6 class (t X. t)
5		vg	. . . . . . 7 set g
6	5	cv 1297	. . . . . 6 class g
7	4, 3, 6	wf 3994	. . . . 5 wff g:(t X. t)-->t
8		vx	. . . . . . . . . . . 12 set x
9	8	cv 1297	. . . . . . . . . . 11 class x
10		vy	. . . . . . . . . . . 12 set y
11	10	cv 1297	. . . . . . . . . . 11 class y
12	9, 11, 6	co 4884	. . . . . . . . . 10 class (xgy)
13		vz	. . . . . . . . . . 11 set z
14	13	cv 1297	. . . . . . . . . 10 class z
15	12, 14, 6	co 4884	. . . . . . . . 9 class ((xgy)gz)
16	11, 14, 6	co 4884	. . . . . . . . . 10 class (ygz)
17	9, 16, 6	co 4884	. . . . . . . . 9 class (xg(ygz))
18	15, 17	wceq 1298	. . . . . . . 8 wff ((xgy)gz) = (xg(ygz))
19	18, 13, 3	wral 2105	. . . . . . 7 wff A.z e. t ((xgy)gz) = (xg(ygz))
20	19, 10, 3	wral 2105	. . . . . 6 wff A.y e. t A.z e. t ((xgy)gz) = (xg(ygz))
21	20, 8, 3	wral 2105	. . . . 5 wff A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz))
22		vu	. . . . . . . . . . 11 set u
23	22	cv 1297	. . . . . . . . . 10 class u
24	23, 9, 6	co 4884	. . . . . . . . 9 class (ugx)
25	24, 9	wceq 1298	. . . . . . . 8 wff (ugx) = x
26	11, 9, 6	co 4884	. . . . . . . . . 10 class (ygx)
27	26, 23	wceq 1298	. . . . . . . . 9 wff (ygx) = u
28	27, 10, 3	wrex 2106	. . . . . . . 8 wff E.y e. t (ygx) = u
29	25, 28	wa 240	. . . . . . 7 wff ((ugx) = x /\ E.y e. t (ygx) = u)
30	29, 8, 3	wral 2105	. . . . . 6 wff A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u)
31	30, 22, 3	wrex 2106	. . . . 5 wff E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u)
32	7, 21, 31	w3a 858	. . . 4 wff (g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))
33	32, 2	wex 1326	. . 3 wff E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))
34	33, 5	cab 1871	. 2 class {g | E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))}
35	1, 34	wceq 1298	1 wff Grp = {g | E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))}

This definition is referenced by:  isgrp 9321

Copyright terms: Public domain