Theorem idafval

Description: Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	idafval.i	|- I = ( IdA ` C )
	idafval.b	|- B = ( Base ` C )
	idafval.c	|- ( ph -> C e. Cat )
	idafval.1	|- .1. = ( Id ` C )
Assertion	idafval	|- ( ph -> I = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		idafval.i	|- I = ( IdA ` C )
2		idafval.b	|- B = ( Base ` C )
3		idafval.c	|- ( ph -> C e. Cat )
4		idafval.1	|- .1. = ( Id ` C )
5		fveq2	|- ( c = C -> ( Base ` c ) = ( Base ` C ) )
6	5 2	eqtr4di	|- ( c = C -> ( Base ` c ) = B )
7		fveq2	|- ( c = C -> ( Id ` c ) = ( Id ` C ) )
8	7 4	eqtr4di	|- ( c = C -> ( Id ` c ) = .1. )
9	8	fveq1d	|- ( c = C -> ( ( Id ` c ) ` x ) = ( .1. ` x ) )
10	9	oteq3d	|- ( c = C -> <. x , x , ( ( Id ` c ) ` x ) >. = <. x , x , ( .1. ` x ) >. )
11	6 10	mpteq12dv	|- ( c = C -> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
12		df-ida	|- IdA = ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )
13	11 12 2	mptfvmpt	|- ( C e. Cat -> ( IdA ` C ) = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
14	3 13	syl	|- ( ph -> ( IdA ` C ) = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
15	1 14	eqtrid	|- ( ph -> I = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )