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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcrcl.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	catcrcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	elcatchom	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		catcrcl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcrcl.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		catcrcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5	1 2 3	catcrcl	⊢ ( 𝜑 → 𝑈 ∈ V )
6	1 2 3 4	catcrcl2	⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
7	6	simpld	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
8	6	simprd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
9	1 4 5 2 7 8	catchom	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 Func 𝑌 ) )
10	3 9	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )