Definition df-gid 7972

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

Assertion

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

Distinct variable group:   u,g,x,y

Detailed syntax breakdown of Definition df-gid

Step	Hyp	Ref	Expression
1		cgi 7968	. 2 class Id
2		vg	. . . . . 6 set g
3	2	cv 952	. . . . 5 class g
4		cgr 7967	. . . . 5 class Grp
5	3, 4	wcel 955	. . . 4 wff g e. Grp
6		vy	. . . . . 6 set y
7	6	cv 952	. . . . 5 class y
8		vu	. . . . . . . . . . 11 set u
9	8	cv 952	. . . . . . . . . 10 class u
10		vx	. . . . . . . . . . 11 set x
11	10	cv 952	. . . . . . . . . 10 class x
12	9, 11, 3	co 3948	. . . . . . . . 9 class (ugx)
13	12, 11	wceq 953	. . . . . . . 8 wff (ugx) = x
14	3	crn 3161	. . . . . . . 8 class ran g
15	13, 10, 14	wral 1637	. . . . . . 7 wff A.x e. ran g(ugx) = x
16	15, 8, 14	crab 1640	. . . . . 6 class {u e. ran g | A.x e. ran g(ugx) = x}
17	16	cuni 2493	. . . . 5 class U.{u e. ran g | A.x e. ran g(ugx) = x}
18	7, 17	wceq 953	. . . 4 wff y = U.{u e. ran g | A.x e. ran g(ugx) = x}
19	5, 18	wa 223	. . 3 wff (g e. Grp /\ y = U.{u e. ran g | A.x e. ran g(ugx) = x})
20	19, 2, 6	copab 2656	. 2 class {<.g, y>. | (g e. Grp /\ y = U.{u e. ran g | A.x e. ran g(ugx) = x})}
21	1, 20	wceq 953	1 wff Id = {<.g, y>. | (g e. Grp /\ y = U.{u e. ran g | A.x e. ran g(ugx) = x})}

This definition is referenced by:  grpidval 7992  0vfval 8163

Copyright terms: Public domain