Theorem prcoffunca2

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

	Ref	Expression
Hypotheses	prcoffunc.r	$$⊢R=D\mathrm{FuncCat}E$$
	prcoffunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
	prcoffunc.s	$$⊢S=C\mathrm{FuncCat}E$$
	prcoffunca.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	prcoffunca2.k	No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. K , L >. ) with typecode |-
Assertion	prcoffunca2	$$⊢\phi \to K\left(R\mathrm{Func}S\right)L$$

Proof

Step	Hyp	Ref	Expression
1		prcoffunc.r	$$⊢R=D\mathrm{FuncCat}E$$
2		prcoffunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
3		prcoffunc.s	$$⊢S=C\mathrm{FuncCat}E$$
4		prcoffunca.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
5		prcoffunca2.k	Could not format ( ph -> ( <. D , E >. -o.F F ) = <. K , L >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. K , L >. ) with typecode |-
6	1 2 3 4	prcoffunca	Could not format ( ph -> ( <. D , E >. -o.F F ) e. ( R Func S ) ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) e. ( R Func S ) ) with typecode |-
7	5 6	eqeltrrd	$$⊢\phi \to ⟨K,L⟩\in \left(R\mathrm{Func}S\right)$$
8		df-br	$$⊢K\left(R\mathrm{Func}S\right)L\leftrightarrow ⟨K,L⟩\in \left(R\mathrm{Func}S\right)$$
9	7 8	sylibr	$$⊢\phi \to K\left(R\mathrm{Func}S\right)L$$