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

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 baseid ⊢ Base = Slot ( Base ‘ ndx )
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 ‘ 𝑅 ) ∈ 𝑈 )