Theorem catchomcl

Description: The Hom-set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl . (Contributed by AV, 14-Oct-2024)

	Ref	Expression
Hypotheses	catcbascl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcbascl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcbascl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	catcbascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	catchomcl	⊢ ( 𝜑 → ( Hom ‘ 𝑋 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		catcbascl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcbascl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		catcbascl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
4		catcbascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		homid	⊢ Hom = Slot ( Hom ‘ ndx )
6	1 2 3 4 5	catcslotelcl	⊢ ( 𝜑 → ( Hom ‘ 𝑋 ) ∈ 𝑈 )