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\mathrm{FuncCat}D$$
	postcofval.r	$$⊢R=D\mathrm{FuncCat}E$$
	postcofval.o	No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) with typecode |-
	postcofval.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
	postcofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	postcofval.k	No typesetting found for |- K = ( ( 1st ` .o. ) ` F ) with typecode |-
	postcofcl.s	$$⊢S=C\mathrm{FuncCat}E$$
Assertion	postcofcl	$$⊢\phi \to K\in \left(Q\mathrm{Func}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		postcofval.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		postcofval.r	$$⊢R=D\mathrm{FuncCat}E$$
3		postcofval.o	Could not format .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) : No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) with typecode |-
4		postcofval.f	$$⊢\phi \to F\in \left(D\mathrm{Func}E\right)$$
5		postcofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		postcofval.k	Could not format K = ( ( 1st ` .o. ) ` F ) : No typesetting found for |- K = ( ( 1st ` .o. ) ` F ) with typecode |-
7		postcofcl.s	$$⊢S=C\mathrm{FuncCat}E$$
8	2	fucbas	$$⊢D\mathrm{Func}E={\mathrm{Base}}_R$$
9	4	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}E\right)2^{nd}\left(F\right)$$
10	9	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
11	9	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
12	2 10 11	fuccat	$$⊢\phi \to R\in \mathrm{Cat}$$
13	1 5 10	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$
14	2 1	oveq12i	$$⊢R{\times }_{c}Q=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
15	14 7 5 10 11	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 |-
16		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
17	3 8 12 13 15 16 4 6	curf1cl	$$⊢\phi \to K\in \left(Q\mathrm{Func}S\right)$$