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