Theorem prcoffunca2

Description: The pre-composition functor is a functor. (Contributed by Zhi Wang, 4-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 ) )
	prcoffunca2.k	|- ( ph -> ( <. D , E >. -o.F F ) = <. K , L >. )
Assertion	prcoffunca2	|- ( ph -> K ( R Func S ) L )

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		prcoffunca2.k	|- ( ph -> ( <. D , E >. -o.F F ) = <. K , L >. )
6	1 2 3 4	prcoffunca	|- ( ph -> ( <. D , E >. -o.F F ) e. ( R Func S ) )
7	5 6	eqeltrrd	|- ( ph -> <. K , L >. e. ( R Func S ) )
8		df-br	|- ( K ( R Func S ) L <-> <. K , L >. e. ( R Func S ) )
9	7 8	sylibr	|- ( ph -> K ( R Func S ) L )