Theorem catcccocl

Description: The composition operation 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	catcccocl	⊢ ( 𝜑 → ( comp ‘ 𝑋 ) ∈ 𝑈 )

Proof

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