Theorem idfu1

Description: Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-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}$$
	idfu1.x	$$⊢\phi \to X\in B$$
Assertion	idfu1	$$⊢\phi \to 1^{st}\left(I\right)\left(X\right)=X$$

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		idfu1.x	$$⊢\phi \to X\in B$$
5	1 2 3	idfu1st	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_B$$
6	5	fveq1d	$$⊢\phi \to 1^{st}\left(I\right)\left(X\right)=\left({\mathrm{I}\upharpoonright }_B\right)\left(X\right)$$
7		fvresi	$$⊢X\in B\to \left({\mathrm{I}\upharpoonright }_B\right)\left(X\right)=X$$
8	4 7	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_B\right)\left(X\right)=X$$
9	6 8	eqtrd	$$⊢\phi \to 1^{st}\left(I\right)\left(X\right)=X$$