This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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