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 
|- ( ph -> U e. WUni )
Assertion ringcbasbas 
|- ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )

Proof

Step Hyp Ref Expression
1 ringcbasbas.r 
 |-  C = ( RingCat ` U )
2 ringcbasbas.b 
 |-  B = ( Base ` C )
3 ringcbasbas.u 
 |-  ( ph -> U e. WUni )
4 1 2 3 ringcbas 
 |-  ( ph -> B = ( U i^i Ring ) )
5 4 eleq2d 
 |-  ( ph -> ( R e. B <-> R e. ( U i^i Ring ) ) )
6 elin 
 |-  ( R e. ( U i^i Ring ) <-> ( R e. U /\ R e. Ring ) )
7 baseid 
 |-  Base = Slot ( Base ` ndx )
8 simpl 
 |-  ( ( U e. WUni /\ R e. U ) -> U e. WUni )
9 simpr 
 |-  ( ( U e. WUni /\ R e. U ) -> R e. U )
10 7 8 9 wunstr 
 |-  ( ( U e. WUni /\ R e. U ) -> ( Base ` R ) e. U )
11 10 ex 
 |-  ( U e. WUni -> ( R e. U -> ( Base ` R ) e. U ) )
12 11 3 syl11 
 |-  ( R e. U -> ( ph -> ( Base ` R ) e. U ) )
13 12 adantr 
 |-  ( ( R e. U /\ R e. Ring ) -> ( ph -> ( Base ` R ) e. U ) )
14 6 13 sylbi 
 |-  ( R e. ( U i^i Ring ) -> ( ph -> ( Base ` R ) e. U ) )
15 14 com12 
 |-  ( ph -> ( R e. ( U i^i Ring ) -> ( Base ` R ) e. U ) )
16 5 15 sylbid 
 |-  ( ph -> ( R e. B -> ( Base ` R ) e. U ) )
17 16 imp 
 |-  ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )