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 e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgi	|- GId
1		vg	|- g
2		cvv	|- _V
3		vu	|- u
4	1	cv	|- g
5	4	crn	|- ran g
6		vx	|- x
7	3	cv	|- u
8	6	cv	|- x
9	7 8 4	co	|- ( u g x )
10	9 8	wceq	|- ( u g x ) = x
11	8 7 4	co	|- ( x g u )
12	11 8	wceq	|- ( x g u ) = x
13	10 12	wa	|- ( ( u g x ) = x /\ ( x g u ) = x )
14	13 6 5	wral	|- A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x )
15	14 3 5	crio	|- ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) )
16	1 2 15	cmpt	|- ( g e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )
17	0 16	wceq	|- GId = ( g e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )