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