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 ⊢ C = RingCat ⁡ U
ringcbasbas.b ⊢ B = Base C
ringcbasbas.u ⊢ φ → U ∈ WUni
Assertion ringcbasbas ⊢ φ ∧ R ∈ B → Base R ∈ U

Proof

Step Hyp Ref Expression
1 ringcbasbas.r ⊢ C = RingCat ⁡ U
2 ringcbasbas.b ⊢ B = Base C
3 ringcbasbas.u ⊢ φ → U ∈ WUni
4 1 2 3 ringcbas ⊢ φ → B = U ∩ Ring
5 4 eleq2d ⊢ φ → R ∈ B ↔ R ∈ U ∩ Ring
6 elin ⊢ R ∈ U ∩ Ring ↔ R ∈ U ∧ R ∈ Ring
7 baseid ⊢ Base = Slot Base ndx
8 simpl ⊢ U ∈ WUni ∧ R ∈ U → U ∈ WUni
9 simpr ⊢ U ∈ WUni ∧ R ∈ U → R ∈ U
10 7 8 9 wunstr ⊢ U ∈ WUni ∧ R ∈ U → Base R ∈ U
11 10 ex ⊢ U ∈ WUni → R ∈ U → Base R ∈ U
12 11 3 syl11 ⊢ R ∈ U → φ → Base R ∈ U
13 12 adantr ⊢ R ∈ U ∧ R ∈ Ring → φ → Base R ∈ U
14 6 13 sylbi ⊢ R ∈ U ∩ Ring → φ → Base R ∈ U
15 14 com12 ⊢ φ → R ∈ U ∩ Ring → Base R ∈ U
16 5 15 sylbid ⊢ φ → R ∈ B → Base R ∈ U
17 16 imp ⊢ φ ∧ R ∈ B → Base R ∈ U