Theorem idfu2nda

Description: Value of the morphism 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 )
	idfu2nda.y	|- ( ph -> Y e. B )
	idfu2nda.h	|- ( ph -> H = ( X ( Hom ` D ) Y ) )
Assertion	idfu2nda	|- ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` H ) )

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		idfu2nda.y	|- ( ph -> Y e. B )
6		idfu2nda.h	|- ( ph -> H = ( X ( Hom ` D ) Y ) )
7		eqid	|- ( Base ` C ) = ( Base ` C )
8	1 2	eqeltrrid	|- ( ph -> ( idFunc ` C ) e. ( D Func E ) )
9		idfurcl	|- ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )
10	8 9	syl	|- ( ph -> C e. Cat )
11		eqid	|- ( Hom ` C ) = ( Hom ` C )
12	1 2 3	idfu1stalem	|- ( ph -> B = ( Base ` C ) )
13	4 12	eleqtrd	|- ( ph -> X e. ( Base ` C ) )
14	5 12	eleqtrd	|- ( ph -> Y e. ( Base ` C ) )
15	1 7 10 11 13 14	idfu2nd	|- ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X ( Hom ` C ) Y ) ) )
16		eqid	|- ( Hom ` D ) = ( Hom ` D )
17	1	idfucl	|- ( C e. Cat -> I e. ( C Func C ) )
18	10 17	syl	|- ( ph -> I e. ( C Func C ) )
19	18	func1st2nd	|- ( ph -> ( 1st ` I ) ( C Func C ) ( 2nd ` I ) )
20	2	func1st2nd	|- ( ph -> ( 1st ` I ) ( D Func E ) ( 2nd ` I ) )
21	19 20	funchomf	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
22	7 11 16 21 13 14	homfeqval	|- ( ph -> ( X ( Hom ` C ) Y ) = ( X ( Hom ` D ) Y ) )
23	6 22	eqtr4d	|- ( ph -> H = ( X ( Hom ` C ) Y ) )
24	23	reseq2d	|- ( ph -> ( _I |` H ) = ( _I |` ( X ( Hom ` C ) Y ) ) )
25	15 24	eqtr4d	|- ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` H ) )