# 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 ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion subrgmre ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubRing}\left({R}\right)\in \mathrm{Moore}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 subrgmre.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 1 subrgss ${⊢}{a}\in \mathrm{SubRing}\left({R}\right)\to {a}\subseteq {B}$
3 velpw ${⊢}{a}\in 𝒫{B}↔{a}\subseteq {B}$
4 2 3 sylibr ${⊢}{a}\in \mathrm{SubRing}\left({R}\right)\to {a}\in 𝒫{B}$
5 4 a1i ${⊢}{R}\in \mathrm{Ring}\to \left({a}\in \mathrm{SubRing}\left({R}\right)\to {a}\in 𝒫{B}\right)$
6 5 ssrdv ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubRing}\left({R}\right)\subseteq 𝒫{B}$
7 1 subrgid ${⊢}{R}\in \mathrm{Ring}\to {B}\in \mathrm{SubRing}\left({R}\right)$
8 subrgint ${⊢}\left({a}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {a}\ne \varnothing \right)\to \bigcap {a}\in \mathrm{SubRing}\left({R}\right)$
9 8 3adant1 ${⊢}\left({R}\in \mathrm{Ring}\wedge {a}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {a}\ne \varnothing \right)\to \bigcap {a}\in \mathrm{SubRing}\left({R}\right)$
10 6 7 9 ismred ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubRing}\left({R}\right)\in \mathrm{Moore}\left({B}\right)$