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

Proof

Step	Hyp	Ref	Expression
1		catcbascl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcbascl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		catcbascl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
4		catcbascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		catcslotelcl.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
6	1 2 3 4	catcbascl	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
7	5 3 6	wunstr	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ 𝑈 )