This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ C = CatCat (U)$
	catcbascl.b	$⊢ B = {Base}_{C}$
	catcbascl.u	$⊢ φ \to U \in WUni$
	catcbascl.x	$⊢ φ \to X \in B$
Assertion	catcccocl	$⊢ φ \to comp (X) \in U$

Proof

Step	Hyp	Ref	Expression
1		catcbascl.c	$⊢ C = CatCat (U)$
2		catcbascl.b	$⊢ B = {Base}_{C}$
3		catcbascl.u	$⊢ φ \to U \in WUni$
4		catcbascl.x	$⊢ φ \to X \in B$
5		ccoid	$⊢ comp = Slot comp (ndx)$
6	1 2 3 4 5	catcslotelcl	$⊢ φ \to comp (X) \in U$