Metamath Proof Explorer

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 = g ∈ GrpOp ⟼ x ∈ ran ⁡ g ⟼ ι z ∈ ran ⁡ g | z g x = GId ⁡ g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgn class inv
1 vg setvar g
2 cgr class GrpOp
3 vx setvar x
4 1 cv setvar g
5 4 crn class ran ⁡ g
6 vz setvar z
7 6 cv setvar z
8 3 cv setvar x
9 7 8 4 co class z g x
10 cgi class GId
11 4 10 cfv class GId ⁡ g
12 9 11 wceq wff z g x = GId ⁡ g
13 12 6 5 crio class ι z ∈ ran ⁡ g | z g x = GId ⁡ g
14 3 5 13 cmpt class x ∈ ran ⁡ g ⟼ ι z ∈ ran ⁡ g | z g x = GId ⁡ g
15 1 2 14 cmpt class g ∈ GrpOp ⟼ x ∈ ran ⁡ g ⟼ ι z ∈ ran ⁡ g | z g x = GId ⁡ g
16 0 15 wceq wff inv = g ∈ GrpOp ⟼ x ∈ ran ⁡ g ⟼ ι z ∈ ran ⁡ g | z g x = GId ⁡ g