Theorem cofucla

Description: The composition of two functors is a functor. Proposition 3.23 of Adamek p. 33. (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	cofucla.f	|- ( ph -> F ( C Func D ) G )
	cofucla.k	|- ( ph -> K ( D Func E ) L )
Assertion	cofucla	|- ( ph -> ( <. K , L >. o.func <. F , G >. ) e. ( C Func E ) )

Proof

Step	Hyp	Ref	Expression
1		cofucla.f	|- ( ph -> F ( C Func D ) G )
2		cofucla.k	|- ( ph -> K ( D Func E ) L )
3		df-br	|- ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
4	1 3	sylib	|- ( ph -> <. F , G >. e. ( C Func D ) )
5		df-br	|- ( K ( D Func E ) L <-> <. K , L >. e. ( D Func E ) )
6	2 5	sylib	|- ( ph -> <. K , L >. e. ( D Func E ) )
7	4 6	cofucl	|- ( ph -> ( <. K , L >. o.func <. F , G >. ) e. ( C Func E ) )