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	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
	cofucla.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
Assertion	cofucla	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩\in \left(C\mathrm{Func}E\right)$$

Proof

Step	Hyp	Ref	Expression
1		cofucla.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
2		cofucla.k	$$⊢\phi \to K\left(D\mathrm{Func}E\right)L$$
3		df-br	$$⊢F\left(C\mathrm{Func}D\right)G\leftrightarrow ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
4	1 3	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
5		df-br	$$⊢K\left(D\mathrm{Func}E\right)L\leftrightarrow ⟨K,L⟩\in \left(D\mathrm{Func}E\right)$$
6	2 5	sylib	$$⊢\phi \to ⟨K,L⟩\in \left(D\mathrm{Func}E\right)$$
7	4 6	cofucl	$$⊢\phi \to ⟨K,L⟩{\circ }_{\mathrm{func}}⟨F,G⟩\in \left(C\mathrm{Func}E\right)$$