Theorem idaval

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 )
	idaval.x	|- ( ph -> X e. B )
Assertion	idaval	|- ( ph -> ( I ` X ) = <. 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		idaval.x	|- ( ph -> X e. B )
6	1 2 3 4	idafval	|- ( ph -> I = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
7		simpr	|- ( ( ph /\ x = X ) -> x = X )
8	7	fveq2d	|- ( ( ph /\ x = X ) -> ( .1. ` x ) = ( .1. ` X ) )
9	7 7 8	oteq123d	|- ( ( ph /\ x = X ) -> <. x , x , ( .1. ` x ) >. = <. X , X , ( .1. ` X ) >. )
10		otex	|- <. X , X , ( .1. ` X ) >. e. _V
11	10	a1i	|- ( ph -> <. X , X , ( .1. ` X ) >. e. _V )
12	6 9 5 11	fvmptd	|- ( ph -> ( I ` X ) = <. X , X , ( .1. ` X ) >. )