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

Metamath Proof Explorer

Theorem catcbascl

Description: 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	catcbascl	$⊢ φ \to 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	1 2 3	catcbas	$⊢ φ \to B = U \cap Cat$
6	4 5	eleqtrd	$⊢ φ \to X \in (U \cap Cat)$
7	6	elin1d	$⊢ φ \to X \in U$