# Metamath Proof Explorer

## 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 ‘ 𝑅 ) ∈ 𝑈 )