Theorem srhmsubclem2

Description: Lemma 2 for srhmsubc . (Contributed by AV, 19-Feb-2020)

	Ref	Expression
Hypotheses	srhmsubc.s	|- A. r e. S r e. Ring
	srhmsubc.c	|- C = ( U i^i S )
Assertion	srhmsubclem2	|- ( ( U e. V /\ X e. C ) -> X e. ( Base ` ( RingCat ` U ) ) )

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	|- A. r e. S r e. Ring
2		srhmsubc.c	|- C = ( U i^i S )
3	1 2	srhmsubclem1	|- ( X e. C -> X e. ( U i^i Ring ) )
4	3	adantl	|- ( ( U e. V /\ X e. C ) -> X e. ( U i^i Ring ) )
5		eqid	|- ( RingCat ` U ) = ( RingCat ` U )
6		eqid	|- ( Base ` ( RingCat ` U ) ) = ( Base ` ( RingCat ` U ) )
7		id	|- ( U e. V -> U e. V )
8	5 6 7	ringcbas	|- ( U e. V -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) )
9	8	adantr	|- ( ( U e. V /\ X e. C ) -> ( Base ` ( RingCat ` U ) ) = ( U i^i Ring ) )
10	4 9	eleqtrrd	|- ( ( U e. V /\ X e. C ) -> X e. ( Base ` ( RingCat ` U ) ) )