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

Metamath Proof Explorer

Theorem elcatchom

Description: A morphism of the category of categories (in a universe) is a functor. See df-catc for the definition of the category Cat, which consists of all categories in the universe u (i.e., " u -small categories", see Definition 3.44. of Adamek p. 39), with functors as the morphisms ( catchom ). (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses catcrcl.c ⊢ C = CatCat ⁡ U
catcrcl.h ⊢ H = Hom ⁡ C
catcrcl.f ⊢ φ → F ∈ X H Y
Assertion elcatchom ⊢ φ → F ∈ X Func Y

Proof

Step Hyp Ref Expression
1 catcrcl.c ⊢ C = CatCat ⁡ U
2 catcrcl.h ⊢ H = Hom ⁡ C
3 catcrcl.f ⊢ φ → F ∈ X H Y
4 eqid ⊢ Base C = Base C
5 1 2 3 catcrcl ⊢ φ → U ∈ V
6 1 2 3 4 catcrcl2 ⊢ φ → X ∈ Base C ∧ Y ∈ Base C
7 6 simpld ⊢ φ → X ∈ Base C
8 6 simprd ⊢ φ → Y ∈ Base C
9 1 4 5 2 7 8 catchom ⊢ φ → X H Y = X Func Y
10 3 9 eleqtrd ⊢ φ → F ∈ X Func Y