Theorem ringcbasbasALTV

Description: An element of the base set of the base set of the category of rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringcbasbasALTV.r	|- C = ( RingCatALTV ` U )
	ringcbasbasALTV.b	|- B = ( Base ` C )
	ringcbasbasALTV.u	|- ( ph -> U e. WUni )
Assertion	ringcbasbasALTV	|- ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )

Proof

Step	Hyp	Ref	Expression
1		ringcbasbasALTV.r	|- C = ( RingCatALTV ` U )
2		ringcbasbasALTV.b	|- B = ( Base ` C )
3		ringcbasbasALTV.u	|- ( ph -> U e. WUni )
4	1 2 3	ringcbasALTV	|- ( 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 )