Theorem srhmsubcALTVlem1

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

	Ref	Expression
Hypotheses	srhmsubcALTV.s	$$⊢\forall r\in Sr\in \mathrm{Ring}$$
	srhmsubcALTV.c	$$⊢C=U\cap S$$
Assertion	srhmsubcALTVlem1	$$⊢\left(U\in V\wedge X\in C\right)\to X\in {\mathrm{Base}}_{\mathrm{RingCatALTV}\left(U\right)}$$

Proof

Step	Hyp	Ref	Expression
1		srhmsubcALTV.s	$$⊢\forall r\in Sr\in \mathrm{Ring}$$
2		srhmsubcALTV.c	$$⊢C=U\cap S$$
3	1 2	srhmsubclem1	$$⊢X\in C\to X\in \left(U\cap \mathrm{Ring}\right)$$
4	3	adantl	$$⊢\left(U\in V\wedge X\in C\right)\to X\in \left(U\cap \mathrm{Ring}\right)$$
5		eqid	$$⊢\mathrm{RingCatALTV}\left(U\right)=\mathrm{RingCatALTV}\left(U\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\mathrm{RingCatALTV}\left(U\right)}={\mathrm{Base}}_{\mathrm{RingCatALTV}\left(U\right)}$$
7		id	$$⊢U\in V\to U\in V$$
8	5 6 7	ringcbasALTV	$$⊢U\in V\to {\mathrm{Base}}_{\mathrm{RingCatALTV}\left(U\right)}=U\cap \mathrm{Ring}$$
9	8	adantr	$$⊢\left(U\in V\wedge X\in C\right)\to {\mathrm{Base}}_{\mathrm{RingCatALTV}\left(U\right)}=U\cap \mathrm{Ring}$$
10	4 9	eleqtrrd	$$⊢\left(U\in V\wedge X\in C\right)\to X\in {\mathrm{Base}}_{\mathrm{RingCatALTV}\left(U\right)}$$