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 = ( idFunc ` C )
	idfu2nda.d	|- ( ph -> I e. ( D Func E ) )
	idfu2nda.b	|- ( ph -> B = ( Base ` D ) )
Assertion	idfu1sta	|- ( ph -> ( 1st ` I ) = ( _I |` B ) )

Proof

Step	Hyp	Ref	Expression
1		idfu2nda.i	|- I = ( idFunc ` C )
2		idfu2nda.d	|- ( ph -> I e. ( D Func E ) )
3		idfu2nda.b	|- ( ph -> B = ( Base ` D ) )
4		eqid	|- ( Base ` C ) = ( Base ` C )
5	1 2	eqeltrrid	|- ( ph -> ( idFunc ` C ) e. ( D Func E ) )
6		idfurcl	|- ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )
7	5 6	syl	|- ( ph -> C e. Cat )
8	1 4 7	idfu1st	|- ( ph -> ( 1st ` I ) = ( _I |` ( Base ` C ) ) )
9	1 2 3	idfu1stalem	|- ( ph -> B = ( Base ` C ) )
10	9	reseq2d	|- ( ph -> ( _I |` B ) = ( _I |` ( Base ` C ) ) )
11	8 10	eqtr4d	|- ( ph -> ( 1st ` I ) = ( _I |` B ) )