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

Metamath Proof Explorer

Theorem setc1strwun

Description: A constructed one-slot structure with the objects of the category of sets as base set in a weak universe. (Contributed by AV, 27-Mar-2020)

		Ref	Expression
	Hypotheses	setc1strwun.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
		setc1strwun.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
		setc1strwun.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
		setc1strwun.o	⊢ ( 𝜑 → ω ∈ 𝑈 )
	Assertion	setc1strwun	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		setc1strwun.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2		setc1strwun.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
3		setc1strwun.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
4		setc1strwun.o	⊢ ( 𝜑 → ω ∈ 𝑈 )
5	1 3	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
6	2 5	eqtr4id	⊢ ( 𝜑 → 𝐶 = 𝑈 )
7	6	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 ↔ 𝑋 ∈ 𝑈 ) )
8	7	biimpa	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ 𝑈 )
9		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ }
10	9 3 4	1strwun	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ∈ 𝑈 )
11	8 10	syldan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ∈ 𝑈 )