Theorem precofcl

Description: The pre-composition functor as a transposed curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	precofval.q	$$⊢Q=C\mathrm{FuncCat}D$$
	precofval.r	$$⊢R=D\mathrm{FuncCat}E$$
	precofval.o	No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
	precofval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	precofval.e	$$⊢\phi \to E\in \mathrm{Cat}$$
	precofval.k	No typesetting found for |- ( ph -> K = ( ( 1st ` .o. ) ` F ) ) with typecode |-
	precofcl.s	$$⊢S=C\mathrm{FuncCat}E$$
Assertion	precofcl	$$⊢\phi \to K\in \left(R\mathrm{Func}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		precofval.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		precofval.r	$$⊢R=D\mathrm{FuncCat}E$$
3		precofval.o	Could not format ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) : No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
4		precofval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
5		precofval.e	$$⊢\phi \to E\in \mathrm{Cat}$$
6		precofval.k	Could not format ( ph -> K = ( ( 1st ` .o. ) ` F ) ) : No typesetting found for |- ( ph -> K = ( ( 1st ` .o. ) ` F ) ) with typecode |-
7		precofcl.s	$$⊢S=C\mathrm{FuncCat}E$$
8	1	fucbas	$$⊢C\mathrm{Func}D={\mathrm{Base}}_Q$$
9		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
10		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
11	9 4 10	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
12	11	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
13	11	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
14	1 12 13	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$
15	2 13 5	fuccat	$$⊢\phi \to R\in \mathrm{Cat}$$
16	2 1	oveq12i	$$⊢R{\times }_{c}Q=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
17	16 7 12 13 5	fucofunca	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func S ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func S ) ) with typecode |-
18	3 8 14 15 17 4 6	tposcurf1cl	$$⊢\phi \to K\in \left(R\mathrm{Func}S\right)$$