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

Step	Hyp	Ref	Expression
1		subrgmre.b	$⊢ B = {Base}_{R}$
2	1	subrgss	$⊢ a \in SubRing (R) \to a \subseteq B$
3		velpw	$⊢ a \in 𝒫 B \leftrightarrow a \subseteq B$
4	2 3	sylibr	$⊢ a \in SubRing (R) \to a \in 𝒫 B$
5	4	a1i	$⊢ R \in Ring \to (a \in SubRing (R) \to a \in 𝒫 B)$
6	5	ssrdv	$⊢ R \in Ring \to SubRing (R) \subseteq 𝒫 B$
7	1	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
8		subrgint	$⊢ (a \subseteq SubRing (R) \land a \neq \emptyset) \to ⋂ a \in SubRing (R)$
9	8	3adant1	$⊢ (R \in Ring \land a \subseteq SubRing (R) \land a \neq \emptyset) \to ⋂ a \in SubRing (R)$
10	6 7 9	ismred	$⊢ R \in Ring \to SubRing (R) \in Moore (B)$

Metamath Proof Explorer