Theorem prcoffunca

Description: The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Hypotheses	prcoffunc.r	|- R = ( D FuncCat E )
	prcoffunc.e	|- ( ph -> E e. Cat )
	prcoffunc.s	|- S = ( C FuncCat E )
	prcoffunca.f	|- ( ph -> F e. ( C Func D ) )
Assertion	prcoffunca	|- ( ph -> ( <. D , E >. -o.F F ) e. ( R Func S ) )

Proof

Step	Hyp	Ref	Expression
1		prcoffunc.r	|- R = ( D FuncCat E )
2		prcoffunc.e	|- ( ph -> E e. Cat )
3		prcoffunc.s	|- S = ( C FuncCat E )
4		prcoffunca.f	|- ( ph -> F e. ( C Func D ) )
5		eqid	|- ( C FuncCat D ) = ( C FuncCat D )
6		eqidd	|- ( ph -> ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) = ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) )
7		eqidd	|- ( ph -> ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` F ) = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` F ) )
8	1 2 5 6 7 4	prcoftposcurfucoa	|- ( ph -> ( <. D , E >. -o.F F ) = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` F ) )
9	5 1 6 4 2 8 3	precofcl	|- ( ph -> ( <. D , E >. -o.F F ) e. ( R Func S ) )