This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → F C Func D G
cofucla.k ⊢ φ → K D Func E L
Assertion cofucla ⊢ φ → K L ∘ func F G ∈ C Func E

Proof

Step Hyp Ref Expression
1 cofucla.f ⊢ φ → F C Func D G
2 cofucla.k ⊢ φ → K D Func E L
3 df-br ⊢ F C Func D G ↔ F G ∈ C Func D
4 1 3 sylib ⊢ φ → F G ∈ C Func D
5 df-br ⊢ K D Func E L ↔ K L ∈ D Func E
6 2 5 sylib ⊢ φ → K L ∈ D Func E
7 4 6 cofucl ⊢ φ → K L ∘ func F G ∈ C Func E