Theorem fucorid2

Description: Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	fucolid.p	|- ( ph -> ( 2nd ` ( <. C , D >. o.F E ) ) = P )
	fucolid.i	|- I = ( Id ` Q )
	fucorid.q	|- Q = ( C FuncCat D )
	fucorid.a	|- ( ph -> A e. ( G ( D Nat E ) H ) )
	fucorid.f	|- ( ph -> F e. ( C Func D ) )
Assertion	fucorid2	|- ( ph -> ( A ( <. G , F >. P <. H , F >. ) ( I ` F ) ) = ( A o. ( 1st ` F ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucolid.p	|- ( ph -> ( 2nd ` ( <. C , D >. o.F E ) ) = P )
2		fucolid.i	|- I = ( Id ` Q )
3		fucorid.q	|- Q = ( C FuncCat D )
4		fucorid.a	|- ( ph -> A e. ( G ( D Nat E ) H ) )
5		fucorid.f	|- ( ph -> F e. ( C Func D ) )
6	1 2 3 4 5	fucorid	|- ( ph -> ( A ( <. G , F >. P <. H , F >. ) ( I ` F ) ) = ( x e. ( Base ` C ) |-> ( A ` ( ( 1st ` F ) ` x ) ) ) )
7		eqid	|- ( D Nat E ) = ( D Nat E )
8	7 4	nat1st2nd	|- ( ph -> A e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( D Nat E ) <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
9		eqid	|- ( Base ` D ) = ( Base ` D )
10	7 8 9	natfn	|- ( ph -> A Fn ( Base ` D ) )
11		dffn2	|- ( A Fn ( Base ` D ) <-> A : ( Base ` D ) --> _V )
12	10 11	sylib	|- ( ph -> A : ( Base ` D ) --> _V )
13		eqid	|- ( Base ` C ) = ( Base ` C )
14		relfunc	|- Rel ( C Func D )
15		1st2ndbr	|- ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
16	14 5 15	sylancr	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
17	13 9 16	funcf1	|- ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
18		fcompt	|- ( ( A : ( Base ` D ) --> _V /\ ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) ) -> ( A o. ( 1st ` F ) ) = ( x e. ( Base ` C ) |-> ( A ` ( ( 1st ` F ) ` x ) ) ) )
19	12 17 18	syl2anc	|- ( ph -> ( A o. ( 1st ` F ) ) = ( x e. ( Base ` C ) |-> ( A ` ( ( 1st ` F ) ` x ) ) ) )
20	6 19	eqtr4d	|- ( ph -> ( A ( <. G , F >. P <. H , F >. ) ( I ` F ) ) = ( A o. ( 1st ` F ) ) )