Theorem idfu1sta

Description: Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

	Ref	Expression
Hypotheses	idfu2nda.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	idfu2nda.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
	idfu2nda.b	$$⊢\phi \to B={\mathrm{Base}}_D$$
Assertion	idfu1sta	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		idfu2nda.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		idfu2nda.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
3		idfu2nda.b	$$⊢\phi \to B={\mathrm{Base}}_D$$
4		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5	1 2	eqeltrrid	$$⊢\phi \to {id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)$$
6		idfurcl	$$⊢{id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)\to C\in \mathrm{Cat}$$
7	5 6	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
8	1 4 7	idfu1st	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_C}$$
9	1 2 3	idfu1stalem	$$⊢\phi \to B={\mathrm{Base}}_C$$
10	9	reseq2d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_B={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_C}$$
11	8 10	eqtr4d	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_B$$