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 
|- ( ph -> F e. ( X H Y ) )
Assertion elcatchom 
|- ( ph -> F e. ( X Func Y ) )

Proof

Step Hyp Ref Expression
1 catcrcl.c 
 |-  C = ( CatCat ` U )
2 catcrcl.h 
 |-  H = ( Hom ` C )
3 catcrcl.f 
 |-  ( ph -> F e. ( X H Y ) )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 1 2 3 catcrcl 
 |-  ( ph -> U e. _V )
6 1 2 3 4 catcrcl2 
 |-  ( ph -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
7 6 simpld 
 |-  ( ph -> X e. ( Base ` C ) )
8 6 simprd 
 |-  ( ph -> Y e. ( Base ` C ) )
9 1 4 5 2 7 8 catchom 
 |-  ( ph -> ( X H Y ) = ( X Func Y ) )
10 3 9 eleqtrd 
 |-  ( ph -> F e. ( X Func Y ) )