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	|- ( ph -> U e. WUni )
	catcbascl.x	|- ( ph -> X e. B )
Assertion	catcbascl	|- ( ph -> X e. U )

Proof

Step	Hyp	Ref	Expression
1		catcbascl.c	|- C = ( CatCat ` U )
2		catcbascl.b	|- B = ( Base ` C )
3		catcbascl.u	|- ( ph -> U e. WUni )
4		catcbascl.x	|- ( ph -> X e. B )
5	1 2 3	catcbas	|- ( ph -> B = ( U i^i Cat ) )
6	4 5	eleqtrd	|- ( ph -> X e. ( U i^i Cat ) )
7	6	elin1d	|- ( ph -> X e. U )