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	|- B = ( Base ` R )
Assertion	subrngmre	|- ( R e. Rng -> ( SubRng ` R ) e. ( Moore ` B ) )

Proof

Step	Hyp	Ref	Expression
1		subrngmre.b	|- B = ( Base ` R )
2	1	subrngss	|- ( a e. ( SubRng ` R ) -> a C_ B )
3		velpw	|- ( a e. ~P B <-> a C_ B )
4	2 3	sylibr	|- ( a e. ( SubRng ` R ) -> a e. ~P B )
5	4	a1i	|- ( R e. Rng -> ( a e. ( SubRng ` R ) -> a e. ~P B ) )
6	5	ssrdv	|- ( R e. Rng -> ( SubRng ` R ) C_ ~P B )
7	1	subrngid	|- ( R e. Rng -> B e. ( SubRng ` R ) )
8		subrngint	|- ( ( a C_ ( SubRng ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRng ` R ) )
9	8	3adant1	|- ( ( R e. Rng /\ a C_ ( SubRng ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRng ` R ) )
10	6 7 9	ismred	|- ( R e. Rng -> ( SubRng ` R ) e. ( Moore ` B ) )