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	4	func1st2nd	|- ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
10	9	funcrcl2	|- ( ph -> D e. Cat )
11	9	funcrcl3	|- ( ph -> E e. Cat )
12	2 10 11	fuccat	|- ( ph -> R e. Cat )
13	1 5 10	fuccat	|- ( ph -> Q e. Cat )
14	2 1	oveq12i	|- ( R Xc. Q ) = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
15	14 7 5 10 11	fucofunca	|- ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func S ) )
16		eqid	|- ( Base ` Q ) = ( Base ` Q )
17	3 8 12 13 15 16 4 6	curf1cl	|- ( ph -> K e. ( Q Func S ) )