Theorem ringcbasbas

Description: An element of the base set of the base set of the category of unital rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020)

	Ref	Expression
Hypotheses	ringcbasbas.r	⊢ 𝐶 = ( RingCat ‘ 𝑈 )
	ringcbasbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	ringcbasbas.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
Assertion	ringcbasbas	⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → ( Base ‘ 𝑅 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ringcbasbas.r	⊢ 𝐶 = ( RingCat ‘ 𝑈 )
2		ringcbasbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		ringcbasbas.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
4	1 2 3	ringcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
5	4	eleq2d	⊢ ( 𝜑 → ( 𝑅 ∈ 𝐵 ↔ 𝑅 ∈ ( 𝑈 ∩ Ring ) ) )
6		elin	⊢ ( 𝑅 ∈ ( 𝑈 ∩ Ring ) ↔ ( 𝑅 ∈ 𝑈 ∧ 𝑅 ∈ Ring ) )
7		df-base	⊢ Base = Slot 1
8		simpl	⊢ ( ( 𝑈 ∈ WUni ∧ 𝑅 ∈ 𝑈 ) → 𝑈 ∈ WUni )
9		simpr	⊢ ( ( 𝑈 ∈ WUni ∧ 𝑅 ∈ 𝑈 ) → 𝑅 ∈ 𝑈 )
10	7 8 9	wunstr	⊢ ( ( 𝑈 ∈ WUni ∧ 𝑅 ∈ 𝑈 ) → ( Base ‘ 𝑅 ) ∈ 𝑈 )
11	10	ex	⊢ ( 𝑈 ∈ WUni → ( 𝑅 ∈ 𝑈 → ( Base ‘ 𝑅 ) ∈ 𝑈 ) )
12	11 3	syl11	⊢ ( 𝑅 ∈ 𝑈 → ( 𝜑 → ( Base ‘ 𝑅 ) ∈ 𝑈 ) )
13	12	adantr	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑅 ∈ Ring ) → ( 𝜑 → ( Base ‘ 𝑅 ) ∈ 𝑈 ) )
14	6 13	sylbi	⊢ ( 𝑅 ∈ ( 𝑈 ∩ Ring ) → ( 𝜑 → ( Base ‘ 𝑅 ) ∈ 𝑈 ) )
15	14	com12	⊢ ( 𝜑 → ( 𝑅 ∈ ( 𝑈 ∩ Ring ) → ( Base ‘ 𝑅 ) ∈ 𝑈 ) )
16	5 15	sylbid	⊢ ( 𝜑 → ( 𝑅 ∈ 𝐵 → ( Base ‘ 𝑅 ) ∈ 𝑈 ) )
17	16	imp	⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → ( Base ‘ 𝑅 ) ∈ 𝑈 )