Theorem postcofcl

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

	Ref	Expression
Hypotheses	postcofval.q	|- Q = ( C FuncCat D )
	postcofval.r	|- R = ( D FuncCat E )
	postcofval.o	|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) )
	postcofval.f	|- ( ph -> F e. ( D Func E ) )
	postcofval.c	|- ( ph -> C e. Cat )
	postcofval.k	|- K = ( ( 1st ` .o. ) ` F )
	postcofcl.s	|- S = ( C FuncCat E )
Assertion	postcofcl	|- ( ph -> K e. ( Q Func S ) )

Proof

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