Theorem gidval

Description: The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	gidval.1	|- X = ran G
Assertion	gidval	|- ( G e. V -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )

Proof

Step	Hyp	Ref	Expression
1		gidval.1	|- X = ran G
2		elex	|- ( G e. V -> G e. _V )
3		rneq	|- ( g = G -> ran g = ran G )
4	3 1	eqtr4di	|- ( g = G -> ran g = X )
5		oveq	|- ( g = G -> ( u g x ) = ( u G x ) )
6	5	eqeq1d	|- ( g = G -> ( ( u g x ) = x <-> ( u G x ) = x ) )
7		oveq	|- ( g = G -> ( x g u ) = ( x G u ) )
8	7	eqeq1d	|- ( g = G -> ( ( x g u ) = x <-> ( x G u ) = x ) )
9	6 8	anbi12d	|- ( g = G -> ( ( ( u g x ) = x /\ ( x g u ) = x ) <-> ( ( u G x ) = x /\ ( x G u ) = x ) ) )
10	4 9	raleqbidv	|- ( g = G -> ( A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) <-> A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
11	4 10	riotaeqbidv	|- ( g = G -> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
12		df-gid	|- GId = ( g e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )
13		riotaex	|- ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) e. _V
14	11 12 13	fvmpt	|- ( G e. _V -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
15	2 14	syl	|- ( G e. V -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )