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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcbascl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcbascl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	catcbascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	catcbascl	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		catcbascl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcbascl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		catcbascl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
4		catcbascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5	1 2 3	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
6	4 5	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
7	6	elin1d	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )