Theorem srhmsubcALTVlem1

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

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

Proof

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