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 )