Theorem ida2

Description: Morphism part of the identity arrow. (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	ida2	|- ( ph -> ( 2nd ` ( I ` 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 5	idaval	|- ( ph -> ( I ` X ) = <. X , X , ( .1. ` X ) >. )
7	6	fveq2d	|- ( ph -> ( 2nd ` ( I ` X ) ) = ( 2nd ` <. X , X , ( .1. ` X ) >. ) )
8		fvex	|- ( .1. ` X ) e. _V
9		ot3rdg	|- ( ( .1. ` X ) e. _V -> ( 2nd ` <. X , X , ( .1. ` X ) >. ) = ( .1. ` X ) )
10	8 9	ax-mp	|- ( 2nd ` <. X , X , ( .1. ` X ) >. ) = ( .1. ` X )
11	7 10	eqtrdi	|- ( ph -> ( 2nd ` ( I ` X ) ) = ( .1. ` X ) )