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

Metamath Proof Explorer

Theorem catcslotelcl

Description: A slot entry 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$
	catcslotelcl.e	$⊢ E = Slot E (ndx)$
Assertion	catcslotelcl	$⊢ φ \to E (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		catcslotelcl.e	$⊢ E = Slot E (ndx)$
6	1 2 3 4	catcbascl	$⊢ φ \to X \in U$
7	5 3 6	wunstr	$⊢ φ \to E (X) \in U$