This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑈 ) ) )