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 FuncCat D )
	precofval.r	|- R = ( D FuncCat E )
	precofval.o	|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
	precofval.f	|- ( ph -> F e. ( C Func D ) )
	precofval.e	|- ( ph -> E e. Cat )
	precofval.k	|- ( ph -> K = ( ( 1st ` .o. ) ` F ) )
	precofcl.s	|- S = ( C FuncCat E )
Assertion	precofcl	|- ( ph -> K e. ( R Func S ) )

Proof

Step	Hyp	Ref	Expression
1		precofval.q	|- Q = ( C FuncCat D )
2		precofval.r	|- R = ( D FuncCat E )
3		precofval.o	|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
4		precofval.f	|- ( ph -> F e. ( C Func D ) )
5		precofval.e	|- ( ph -> E e. Cat )
6		precofval.k	|- ( ph -> K = ( ( 1st ` .o. ) ` F ) )
7		precofcl.s	|- S = ( C FuncCat E )
8	1	fucbas	|- ( C Func D ) = ( Base ` Q )
9		relfunc	|- Rel ( C Func D )
10		1st2ndbr	|- ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
11	9 4 10	sylancr	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
12	11	funcrcl2	|- ( ph -> C e. Cat )
13	11	funcrcl3	|- ( ph -> D e. Cat )
14	1 12 13	fuccat	|- ( ph -> Q e. Cat )
15	2 13 5	fuccat	|- ( ph -> R e. Cat )
16	2 1	oveq12i	|- ( R Xc. Q ) = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
17	16 7 12 13 5	fucofunca	|- ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func S ) )
18	3 8 14 15 17 4 6	tposcurf1cl	|- ( ph -> K e. ( R Func S ) )