Definition df-ginv

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.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgn	⊢ inv
1		vg	⊢ 𝑔
2		cgr	⊢ GrpOp
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑔
5	4	crn	⊢ ran 𝑔
6		vz	⊢ 𝑧
7	6	cv	⊢ 𝑧
8	3	cv	⊢ 𝑥
9	7 8 4	co	⊢ ( 𝑧 𝑔 𝑥 )
10		cgi	⊢ GId
11	4 10	cfv	⊢ ( GId ‘ 𝑔 )
12	9 11	wceq	⊢ ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 )
13	12 6 5	crio	⊢ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) )
14	3 5 13	cmpt	⊢ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) )
15	1 2 14	cmpt	⊢ ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) )
16	0 15	wceq	⊢ inv = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 ↦ ( ℩ 𝑧 ∈ ran 𝑔 ( 𝑧 𝑔 𝑥 ) = ( GId ‘ 𝑔 ) ) ) )