Definition df-gid 9317

Description: Define a function that maps a group operation to the group's identity element.

Assertion

Ref	Expression
df-gid	|- Id = {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}

Distinct variable group:   u,g,x,y

Detailed syntax breakdown of Definition df-gid

Step	Hyp	Ref	Expression
1		cgi 9312	. 2 class Id
2		vy	. . . . 5 set y
3	2	cv 1297	. . . 4 class y
4		vu	. . . . . . . . . . 11 set u
5	4	cv 1297	. . . . . . . . . 10 class u
6		vx	. . . . . . . . . . 11 set x
7	6	cv 1297	. . . . . . . . . 10 class x
8		vg	. . . . . . . . . . 11 set g
9	8	cv 1297	. . . . . . . . . 10 class g
10	5, 7, 9	co 4884	. . . . . . . . 9 class (ugx)
11	10, 7	wceq 1298	. . . . . . . 8 wff (ugx) = x
12	7, 5, 9	co 4884	. . . . . . . . 9 class (xgu)
13	12, 7	wceq 1298	. . . . . . . 8 wff (xgu) = x
14	11, 13	wa 240	. . . . . . 7 wff ((ugx) = x /\ (xgu) = x)
15	9	crn 3987	. . . . . . 7 class ran g
16	14, 6, 15	wral 2105	. . . . . 6 wff A.x e. ran g((ugx) = x /\ (xgu) = x)
17	16, 4, 15	crab 2108	. . . . 5 class {u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}
18	17	cuni 3177	. . . 4 class U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}
19	3, 18	wceq 1298	. . 3 wff y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}
20	19, 8, 2	copab 3395	. 2 class {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}
21	1, 20	wceq 1298	1 wff Id = {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}

This definition is referenced by:  gid0 9338  fungid 9339  grpidvallem 9341  grpidval 9342  idrval 10374

Copyright terms: Public domain