Theorem fucoridid

Description: Horizontal composition with the identity natural transformation of the identity functor leaves a natural transformation unchanged. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fucoridid.p	|- ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = P )
	fucoridid.q	|- Q = ( C FuncCat C )
	fucoridid.j	|- J = ( Id ` Q )
	fucoridid.i	|- I = ( idFunc ` C )
	fucoridid.c	|- ( ph -> C e. Cat )
	fucoridid.a	|- ( ph -> A e. ( G ( C Nat E ) H ) )
Assertion	fucoridid	|- ( ph -> ( A ( <. G , I >. P <. H , I >. ) ( J ` I ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		fucoridid.p	|- ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = P )
2		fucoridid.q	|- Q = ( C FuncCat C )
3		fucoridid.j	|- J = ( Id ` Q )
4		fucoridid.i	|- I = ( idFunc ` C )
5		fucoridid.c	|- ( ph -> C e. Cat )
6		fucoridid.a	|- ( ph -> A e. ( G ( C Nat E ) H ) )
7	4	idfucl	|- ( C e. Cat -> I e. ( C Func C ) )
8	5 7	syl	|- ( ph -> I e. ( C Func C ) )
9	1 3 2 6 8	fucorid2	|- ( ph -> ( A ( <. G , I >. P <. H , I >. ) ( J ` I ) ) = ( A o. ( 1st ` I ) ) )
10		eqid	|- ( Base ` C ) = ( Base ` C )
11	4 10 5	idfu1st	|- ( ph -> ( 1st ` I ) = ( _I |` ( Base ` C ) ) )
12	11	coeq2d	|- ( ph -> ( A o. ( 1st ` I ) ) = ( A o. ( _I |` ( Base ` C ) ) ) )
13		eqid	|- ( C Nat E ) = ( C Nat E )
14	13 10 6	natfn2	|- ( ph -> A Fn ( Base ` C ) )
15		dffn2	|- ( A Fn ( Base ` C ) <-> A : ( Base ` C ) --> _V )
16	14 15	sylib	|- ( ph -> A : ( Base ` C ) --> _V )
17		fcoi1	|- ( A : ( Base ` C ) --> _V -> ( A o. ( _I |` ( Base ` C ) ) ) = A )
18	16 17	syl	|- ( ph -> ( A o. ( _I |` ( Base ` C ) ) ) = A )
19	9 12 18	3eqtrd	|- ( ph -> ( A ( <. G , I >. P <. H , I >. ) ( J ` I ) ) = A )