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=\mathrm{CatCat}\left(U\right)$$
	catcrcl.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	catcrcl.f	$$⊢\phi \to F\in \left(XHY\right)$$
Assertion	elcatchom	$$⊢\phi \to F\in \left(X\mathrm{Func}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		catcrcl.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		catcrcl.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		catcrcl.f	$$⊢\phi \to F\in \left(XHY\right)$$
4		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5	1 2 3	catcrcl	$$⊢\phi \to U\in \mathrm{V}$$
6	1 2 3 4	catcrcl2	$$⊢\phi \to \left(X\in {\mathrm{Base}}_C\wedge Y\in {\mathrm{Base}}_C\right)$$
7	6	simpld	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
8	6	simprd	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
9	1 4 5 2 7 8	catchom	$$⊢\phi \to XHY=X\mathrm{Func}Y$$
10	3 9	eleqtrd	$$⊢\phi \to F\in \left(X\mathrm{Func}Y\right)$$