Theorem srhmsubcALTVlem1

Description: Lemma 1 for srhmsubcALTV . (Contributed by AV, 19-Feb-2020) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		srhmsubcALTV.s	|- A. r e. S r e. Ring
2		srhmsubcALTV.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	|- ( RingCatALTV ` U ) = ( RingCatALTV ` U )
6		eqid	|- ( Base ` ( RingCatALTV ` U ) ) = ( Base ` ( RingCatALTV ` U ) )
7		id	|- ( U e. V -> U e. V )
8	5 6 7	ringcbasALTV	|- ( U e. V -> ( Base ` ( RingCatALTV ` U ) ) = ( U i^i Ring ) )
9	8	adantr	|- ( ( U e. V /\ X e. C ) -> ( Base ` ( RingCatALTV ` U ) ) = ( U i^i Ring ) )
10	4 9	eleqtrrd	|- ( ( U e. V /\ X e. C ) -> X e. ( Base ` ( RingCatALTV ` U ) ) )