Definition df-ginv 9318

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

Assertion

Ref	Expression
df-ginv	|- inv = {<.g, f>. | (g e. Grp /\ f = {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})})}

Distinct variable group:   f,g,x,y,z

Detailed syntax breakdown of Definition df-ginv

Step	Hyp	Ref	Expression
1		cgn 9313	. 2 class inv
2		vg	. . . . . 6 set g
3	2	cv 1297	. . . . 5 class g
4		cgr 9311	. . . . 5 class Grp
5	3, 4	wcel 1300	. . . 4 wff g e. Grp
6		vf	. . . . . 6 set f
7	6	cv 1297	. . . . 5 class f
8		vx	. . . . . . . . 9 set x
9	8	cv 1297	. . . . . . . 8 class x
10	3	crn 3987	. . . . . . . 8 class ran g
11	9, 10	wcel 1300	. . . . . . 7 wff x e. ran g
12		vy	. . . . . . . . 9 set y
13	12	cv 1297	. . . . . . . 8 class y
14		vz	. . . . . . . . . . . . 13 set z
15	14	cv 1297	. . . . . . . . . . . 12 class z
16	15, 9, 3	co 4884	. . . . . . . . . . 11 class (zgx)
17		cgi 9312	. . . . . . . . . . . 12 class Id
18	3, 17	cfv 3998	. . . . . . . . . . 11 class (Id` g)
19	16, 18	wceq 1298	. . . . . . . . . 10 wff (zgx) = (Id` g)
20	19, 14, 10	crab 2108	. . . . . . . . 9 class {z e. ran g | (zgx) = (Id` g)}
21	20	cuni 3177	. . . . . . . 8 class U.{z e. ran g | (zgx) = (Id` g)}
22	13, 21	wceq 1298	. . . . . . 7 wff y = U.{z e. ran g | (zgx) = (Id` g)}
23	11, 22	wa 240	. . . . . 6 wff (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})
24	23, 8, 12	copab 3395	. . . . 5 class {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})}
25	7, 24	wceq 1298	. . . 4 wff f = {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})}
26	5, 25	wa 240	. . 3 wff (g e. Grp /\ f = {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})})
27	26, 2, 6	copab 3395	. 2 class {<.g, f>. | (g e. Grp /\ f = {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})})}
28	1, 27	wceq 1298	1 wff inv = {<.g, f>. | (g e. Grp /\ f = {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})})}

This definition is referenced by:  grpinvfval 9350

Copyright terms: Public domain