Theorem idfu1a

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$$
	idfu2nda.x	$$⊢\phi \to X\in B$$
Assertion	idfu1a	$$⊢\phi \to 1^{st}\left(I\right)\left(X\right)=X$$

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		idfu2nda.x	$$⊢\phi \to X\in B$$
5		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
6	1 2	eqeltrrid	$$⊢\phi \to {id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)$$
7		idfurcl	$$⊢{id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)\to C\in \mathrm{Cat}$$
8	6 7	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
9	1 2 3	idfu1stalem	$$⊢\phi \to B={\mathrm{Base}}_C$$
10	4 9	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
11	1 5 8 10	idfu1	$$⊢\phi \to 1^{st}\left(I\right)\left(X\right)=X$$