Definition df-grpo 27347

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. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-grpo	|- GrpOp = { g | E. t ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) ) }

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

Detailed syntax breakdown of Definition df-grpo

Step	Hyp	Ref	Expression
1		cgr 27343	. 2 class GrpOp
2		vt	. . . . . . . 8 setvar t
3	2	cv 1482	. . . . . . 7 class t
4	3, 3	cxp 5112	. . . . . 6 class ( t X. t )
5		vg	. . . . . . 7 setvar g
6	5	cv 1482	. . . . . 6 class g
7	4, 3, 6	wf 5884	. . . . 5 wff g : ( t X. t ) --> t
8		vx	. . . . . . . . . . . 12 setvar x
9	8	cv 1482	. . . . . . . . . . 11 class x
10		vy	. . . . . . . . . . . 12 setvar y
11	10	cv 1482	. . . . . . . . . . 11 class y
12	9, 11, 6	co 6650	. . . . . . . . . 10 class ( x g y )
13		vz	. . . . . . . . . . 11 setvar z
14	13	cv 1482	. . . . . . . . . 10 class z
15	12, 14, 6	co 6650	. . . . . . . . 9 class ( ( x g y ) g z )
16	11, 14, 6	co 6650	. . . . . . . . . 10 class ( y g z )
17	9, 16, 6	co 6650	. . . . . . . . 9 class ( x g ( y g z ) )
18	15, 17	wceq 1483	. . . . . . . 8 wff ( ( x g y ) g z ) = ( x g ( y g z ) )
19	18, 13, 3	wral 2912	. . . . . . 7 wff A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) )
20	19, 10, 3	wral 2912	. . . . . 6 wff A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) )
21	20, 8, 3	wral 2912	. . . . 5 wff A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) )
22		vu	. . . . . . . . . . 11 setvar u
23	22	cv 1482	. . . . . . . . . 10 class u
24	23, 9, 6	co 6650	. . . . . . . . 9 class ( u g x )
25	24, 9	wceq 1483	. . . . . . . 8 wff ( u g x ) = x
26	11, 9, 6	co 6650	. . . . . . . . . 10 class ( y g x )
27	26, 23	wceq 1483	. . . . . . . . 9 wff ( y g x ) = u
28	27, 10, 3	wrex 2913	. . . . . . . 8 wff E. y e. t ( y g x ) = u
29	25, 28	wa 384	. . . . . . 7 wff ( ( u g x ) = x /\ E. y e. t ( y g x ) = u )
30	29, 8, 3	wral 2912	. . . . . 6 wff A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u )
31	30, 22, 3	wrex 2913	. . . . 5 wff E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u )
32	7, 21, 31	w3a 1037	. . . 4 wff ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) )
33	32, 2	wex 1704	. . 3 wff E. t ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) )
34	33, 5	cab 2608	. 2 class { g | E. t ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) ) }
35	1, 34	wceq 1483	1 wff GrpOp = { g | E. t ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) ) }

This definition is referenced by:  isgrpo  27351