Definition df-gid 10335

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 10330	. 2 class Id
2		vy	. . . . 5 set y
3	2	cv 1614	. . . 4 class y
4		vu	. . . . . . . . . . 11 set u
5	4	cv 1614	. . . . . . . . . 10 class u
6		vx	. . . . . . . . . . 11 set x
7	6	cv 1614	. . . . . . . . . 10 class x
8		vg	. . . . . . . . . . 11 set g
9	8	cv 1614	. . . . . . . . . 10 class g
10	5, 7, 9	co 5020	. . . . . . . . 9 class (ugx)
11	10, 7	wceq 1615	. . . . . . . 8 wff (ugx) = x
12	7, 5, 9	co 5020	. . . . . . . . 9 class (xgu)
13	12, 7	wceq 1615	. . . . . . . 8 wff (xgu) = x
14	11, 13	wa 433	. . . . . . 7 wff ((ugx) = x /\ (xgu) = x)
15	9	crn 4152	. . . . . . 7 class ran g
16	14, 6, 15	wral 2385	. . . . . 6 wff A.x e. ran g((ugx) = x /\ (xgu) = x)
17	16, 4, 15	crab 2388	. . . . 5 class {u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}
18	17	cuni 3398	. . . 4 class U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}
19	3, 18	wceq 1615	. . 3 wff y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}
20	19, 8, 2	copab 3597	. 2 class {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}
21	1, 20	wceq 1615	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 10359  fungid 10360  grpidvallem 10362  grpoidval 10363  idrval 11370

Copyright terms: Public domain