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

Metamath Proof Explorer

Theorem subrgmre

Description: The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypothesis subrgmre.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion subrgmre ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) ∈ ( Moore ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subrgmre.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 1 subrgss ⊢ ( 𝑎 ∈ ( SubRing ‘ 𝑅 ) → 𝑎 ⊆ 𝐵 )
3 velpw ⊢ ( 𝑎 ∈ 𝒫 𝐵 ↔ 𝑎 ⊆ 𝐵 )
4 2 3 sylibr ⊢ ( 𝑎 ∈ ( SubRing ‘ 𝑅 ) → 𝑎 ∈ 𝒫 𝐵 )
5 4 a1i ⊢ ( 𝑅 ∈ Ring → ( 𝑎 ∈ ( SubRing ‘ 𝑅 ) → 𝑎 ∈ 𝒫 𝐵 ) )
6 5 ssrdv ⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) ⊆ 𝒫 𝐵 )
7 1 subrgid ⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
8 subrgint ⊢ ( ( 𝑎 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑎 ∈ ( SubRing ‘ 𝑅 ) )
9 8 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑎 ∈ ( SubRing ‘ 𝑅 ) )
10 6 7 9 ismred ⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) ∈ ( Moore ‘ 𝐵 ) )