subrngmre

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

		Ref	Expression
	Hypothesis	subrngmre.b	$⊢ B = {Base}_{R}$
	Assertion	subrngmre	$⊢ R \in Rng \to SubRng (R) \in Moore (B)$

Step	Hyp	Ref	Expression
1		subrngmre.b	$⊢ B = {Base}_{R}$
2	1	subrngss	$⊢ a \in SubRng (R) \to a \subseteq B$
3		velpw	$⊢ a \in 𝒫 B \leftrightarrow a \subseteq B$
4	2 3	sylibr	$⊢ a \in SubRng (R) \to a \in 𝒫 B$
5	4	a1i	$⊢ R \in Rng \to (a \in SubRng (R) \to a \in 𝒫 B)$
6	5	ssrdv	$⊢ R \in Rng \to SubRng (R) \subseteq 𝒫 B$
7	1	subrngid	$⊢ R \in Rng \to B \in SubRng (R)$
8		subrngint	$⊢ (a \subseteq SubRng (R) \land a \neq \emptyset) \to ⋂ a \in SubRng (R)$
9	8	3adant1	$⊢ (R \in Rng \land a \subseteq SubRng (R) \land a \neq \emptyset) \to ⋂ a \in SubRng (R)$
10	6 7 9	ismred	$⊢ R \in Rng \to SubRng (R) \in Moore (B)$

Metamath Proof Explorer