Theorem srhmsubclem2

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

	Ref	Expression
Hypotheses	srhmsubc.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
	srhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
Assertion	srhmsubclem2	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
2		srhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
3	1 2	srhmsubclem1	⊢ ( 𝑋 ∈ 𝐶 → 𝑋 ∈ ( 𝑈 ∩ Ring ) )
4	3	adantl	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( 𝑈 ∩ Ring ) )
5		eqid	⊢ ( RingCat ‘ 𝑈 ) = ( RingCat ‘ 𝑈 )
6		eqid	⊢ ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( Base ‘ ( RingCat ‘ 𝑈 ) )
7		id	⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉 )
8	5 6 7	ringcbas	⊢ ( 𝑈 ∈ 𝑉 → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Ring ) )
9	8	adantr	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Ring ) )
10	4 9	eleqtrrd	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )