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={id}_{\mathrm{func}}\left(C\right)$$
	idfuval.b	$$⊢B={\mathrm{Base}}_C$$
	idfuval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	idfuval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	idfu2nd.x	$$⊢\phi \to X\in B$$
	idfu2nd.y	$$⊢\phi \to Y\in B$$
	idfu2.f	$$⊢\phi \to F\in \left(XHY\right)$$
Assertion	idfu2	$$⊢\phi \to \left(X{2}^{nd}\left(I\right)Y\right)\left(F\right)=F$$

Proof

Step	Hyp	Ref	Expression
1		idfuval.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		idfuval.b	$$⊢B={\mathrm{Base}}_C$$
3		idfuval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		idfuval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		idfu2nd.x	$$⊢\phi \to X\in B$$
6		idfu2nd.y	$$⊢\phi \to Y\in B$$
7		idfu2.f	$$⊢\phi \to F\in \left(XHY\right)$$
8	1 2 3 4 5 6	idfu2nd	$$⊢\phi \to X{2}^{nd}\left(I\right)Y={\mathrm{I}\upharpoonright }_{\left(XHY\right)}$$
9	8	fveq1d	$$⊢\phi \to \left(X{2}^{nd}\left(I\right)Y\right)\left(F\right)=\left({\mathrm{I}\upharpoonright }_{\left(XHY\right)}\right)\left(F\right)$$
10		fvresi	$$⊢F\in \left(XHY\right)\to \left({\mathrm{I}\upharpoonright }_{\left(XHY\right)}\right)\left(F\right)=F$$
11	7 10	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{\left(XHY\right)}\right)\left(F\right)=F$$
12	9 11	eqtrd	$$⊢\phi \to \left(X{2}^{nd}\left(I\right)Y\right)\left(F\right)=F$$