Theorem idfu2

Description: Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	idfuval.i	|- I = ( idFunc ` C )
	idfuval.b	|- B = ( Base ` C )
	idfuval.c	|- ( ph -> C e. Cat )
	idfuval.h	|- H = ( Hom ` C )
	idfu2nd.x	|- ( ph -> X e. B )
	idfu2nd.y	|- ( ph -> Y e. B )
	idfu2.f	|- ( ph -> F e. ( X H Y ) )
Assertion	idfu2	|- ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = F )

Proof

Step	Hyp	Ref	Expression
1		idfuval.i	|- I = ( idFunc ` C )
2		idfuval.b	|- B = ( Base ` C )
3		idfuval.c	|- ( ph -> C e. Cat )
4		idfuval.h	|- H = ( Hom ` C )
5		idfu2nd.x	|- ( ph -> X e. B )
6		idfu2nd.y	|- ( ph -> Y e. B )
7		idfu2.f	|- ( ph -> F e. ( X H Y ) )
8	1 2 3 4 5 6	idfu2nd	|- ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X H Y ) ) )
9	8	fveq1d	|- ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = ( ( _I |` ( X H Y ) ) ` F ) )
10		fvresi	|- ( F e. ( X H Y ) -> ( ( _I |` ( X H Y ) ) ` F ) = F )
11	7 10	syl	|- ( ph -> ( ( _I |` ( X H Y ) ) ` F ) = F )
12	9 11	eqtrd	|- ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = F )