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

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		idfu2nda.x	|- ( ph -> X e. B )
5		eqid	|- ( Base ` C ) = ( Base ` C )
6	1 2	eqeltrrid	|- ( ph -> ( idFunc ` C ) e. ( D Func E ) )
7		idfurcl	|- ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )
8	6 7	syl	|- ( ph -> C e. Cat )
9	1 2 3	idfu1stalem	|- ( ph -> B = ( Base ` C ) )
10	4 9	eleqtrd	|- ( ph -> X e. ( Base ` C ) )
11	1 5 8 10	idfu1	|- ( ph -> ( ( 1st ` I ) ` X ) = X )