Metamath Proof Explorer

Definition df-gid

Description: Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion df-gid ⊢ GId = g ∈ V ⟼ ι u ∈ ran ⁡ g | ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgi class GId
1 vg setvar g
2 cvv class V
3 vu setvar u
4 1 cv setvar g
5 4 crn class ran ⁡ g
6 vx setvar x
7 3 cv setvar u
8 6 cv setvar x
9 7 8 4 co class u g x
10 9 8 wceq wff u g x = x
11 8 7 4 co class x g u
12 11 8 wceq wff x g u = x
13 10 12 wa wff u g x = x ∧ x g u = x
14 13 6 5 wral wff ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x
15 14 3 5 crio class ι u ∈ ran ⁡ g | ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x
16 1 2 15 cmpt class g ∈ V ⟼ ι u ∈ ran ⁡ g | ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x
17 0 16 wceq wff GId = g ∈ V ⟼ ι u ∈ ran ⁡ g | ∀ x ∈ ran ⁡ g u g x = x ∧ x g u = x