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 = ( Base ` R )
Assertion	subrgmre	|- ( R e. Ring -> ( SubRing ` R ) e. ( Moore ` B ) )

Proof

Step	Hyp	Ref	Expression
1		subrgmre.b	|- B = ( Base ` R )
2	1	subrgss	|- ( a e. ( SubRing ` R ) -> a C_ B )
3		velpw	|- ( a e. ~P B <-> a C_ B )
4	2 3	sylibr	|- ( a e. ( SubRing ` R ) -> a e. ~P B )
5	4	a1i	|- ( R e. Ring -> ( a e. ( SubRing ` R ) -> a e. ~P B ) )
6	5	ssrdv	|- ( R e. Ring -> ( SubRing ` R ) C_ ~P B )
7	1	subrgid	|- ( R e. Ring -> B e. ( SubRing ` R ) )
8		subrgint	|- ( ( a C_ ( SubRing ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRing ` R ) )
9	8	3adant1	|- ( ( R e. Ring /\ a C_ ( SubRing ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRing ` R ) )
10	6 7 9	ismred	|- ( R e. Ring -> ( SubRing ` R ) e. ( Moore ` B ) )