Theorem srhmsubclem2

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

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

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	$$⊢\forall r\in Sr\in \mathrm{Ring}$$
2		srhmsubc.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{RingCat}\left(U\right)=\mathrm{RingCat}\left(U\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\mathrm{RingCat}\left(U\right)}={\mathrm{Base}}_{\mathrm{RingCat}\left(U\right)}$$
7		id	$$⊢U\in V\to U\in V$$
8	5 6 7	ringcbas	$$⊢U\in V\to {\mathrm{Base}}_{\mathrm{RingCat}\left(U\right)}=U\cap \mathrm{Ring}$$
9	8	adantr	$$⊢\left(U\in V\wedge X\in C\right)\to {\mathrm{Base}}_{\mathrm{RingCat}\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{RingCat}\left(U\right)}$$