Definition df-ginv 30514

Description: Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-ginv	⊢ inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))

Distinct variable group:   𝑥,𝑔,𝑧

Detailed syntax breakdown of Definition df-ginv

Step	Hyp	Ref	Expression
1		cgn 30510	. 2 class inv
2		vg	. . 3 setvar 𝑔
3		cgr 30508	. . 3 class GrpOp
4		vx	. . . 4 setvar 𝑥
5	2	cv 1539	. . . . 5 class 𝑔
6	5	crn 5686	. . . 4 class ran 𝑔
7		vz	. . . . . . . 8 setvar 𝑧
8	7	cv 1539	. . . . . . 7 class 𝑧
9	4	cv 1539	. . . . . . 7 class 𝑥
10	8, 9, 5	co 7431	. . . . . 6 class (𝑧𝑔𝑥)
11		cgi 30509	. . . . . . 7 class GId
12	5, 11	cfv 6561	. . . . . 6 class (GId‘𝑔)
13	10, 12	wceq 1540	. . . . 5 wff (𝑧𝑔𝑥) = (GId‘𝑔)
14	13, 7, 6	crio 7387	. . . 4 class (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))
15	4, 6, 14	cmpt 5225	. . 3 class (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔)))
16	2, 3, 15	cmpt 5225	. 2 class (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))
17	1, 16	wceq 1540	1 wff inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))

This definition is referenced by:  grpoinvfval  30541