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	$$⊢C=\mathrm{CatCat}\left(U\right)$$
	catcbascl.b	$$⊢B={\mathrm{Base}}_C$$
	catcbascl.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	catcbascl.x	$$⊢\phi \to X\in B$$
Assertion	catchomcl	$$⊢\phi \to \mathrm{Hom}\left(X\right)\in U$$

Proof

Step	Hyp	Ref	Expression
1		catcbascl.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		catcbascl.b	$$⊢B={\mathrm{Base}}_C$$
3		catcbascl.u	$$⊢\phi \to U\in \mathrm{WUni}$$
4		catcbascl.x	$$⊢\phi \to X\in B$$
5		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
6	1 2 3 4 5	catcslotelcl	$$⊢\phi \to \mathrm{Hom}\left(X\right)\in U$$