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

Metamath Proof Explorer

Theorem subrngmre

Description: The subrings of a non-unital ring are a Moore system. (Contributed by AV, 15-Feb-2025)

Ref Expression
Hypothesis subrngmre.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion subrngmre ( 𝑅 ∈ Rng → ( SubRng ‘ 𝑅 ) ∈ ( Moore ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subrngmre.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 1 subrngss ⊢ ( 𝑎 ∈ ( SubRng ‘ 𝑅 ) → 𝑎 ⊆ 𝐵 )
3 velpw ⊢ ( 𝑎 ∈ 𝒫 𝐵 ↔ 𝑎 ⊆ 𝐵 )
4 2 3 sylibr ⊢ ( 𝑎 ∈ ( SubRng ‘ 𝑅 ) → 𝑎 ∈ 𝒫 𝐵 )
5 4 a1i ⊢ ( 𝑅 ∈ Rng → ( 𝑎 ∈ ( SubRng ‘ 𝑅 ) → 𝑎 ∈ 𝒫 𝐵 ) )
6 5 ssrdv ⊢ ( 𝑅 ∈ Rng → ( SubRng ‘ 𝑅 ) ⊆ 𝒫 𝐵 )
7 1 subrngid ⊢ ( 𝑅 ∈ Rng → 𝐵 ∈ ( SubRng ‘ 𝑅 ) )
8 subrngint ⊢ ( ( 𝑎 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑎 ∈ ( SubRng ‘ 𝑅 ) )
9 8 3adant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑎 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑎 ∈ ( SubRng ‘ 𝑅 ) )
10 6 7 9 ismred ⊢ ( 𝑅 ∈ Rng → ( SubRng ‘ 𝑅 ) ∈ ( Moore ‘ 𝐵 ) )