srhmsubclem2

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

Step	Hyp	Ref	Expression
1		srhmsubc.s	$⊢ \forall r \in S r \in Ring$
2		srhmsubc.c	$⊢ C = U \cap S$
3	1 2	srhmsubclem1	$⊢ X \in C \to X \in (U \cap Ring)$
4	3	adantl	$⊢ (U \in V \land X \in C) \to X \in (U \cap Ring)$
5		eqid	$⊢ RingCat (U) = RingCat (U)$
6		eqid	$⊢ {Base}_{RingCat (U)} = {Base}_{RingCat (U)}$
7		id	$⊢ U \in V \to U \in V$
8	5 6 7	ringcbas	$⊢ U \in V \to {Base}_{RingCat (U)} = U \cap Ring$
9	8	adantr	$⊢ (U \in V \land X \in C) \to {Base}_{RingCat (U)} = U \cap Ring$
10	4 9	eleqtrrd	$⊢ (U \in V \land X \in C) \to X \in {Base}_{RingCat (U)}$

Metamath Proof Explorer