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={\mathrm{Base}}_R$$
Assertion	subrngmre	Could not format assertion : No typesetting found for |- ( R e. Rng -> ( SubRng ` R ) e. ( Moore ` B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subrngmre.b	$$⊢B={\mathrm{Base}}_R$$
2	1	subrngss	Could not format ( a e. ( SubRng ` R ) -> a C_ B ) : No typesetting found for |- ( a e. ( SubRng ` R ) -> a C_ B ) with typecode |-
3		velpw	$$⊢a\in 𝒫B\leftrightarrow a\subseteq B$$
4	2 3	sylibr	Could not format ( a e. ( SubRng ` R ) -> a e. ~P B ) : No typesetting found for |- ( a e. ( SubRng ` R ) -> a e. ~P B ) with typecode |-
5	4	a1i	Could not format ( R e. Rng -> ( a e. ( SubRng ` R ) -> a e. ~P B ) ) : No typesetting found for |- ( R e. Rng -> ( a e. ( SubRng ` R ) -> a e. ~P B ) ) with typecode |-
6	5	ssrdv	Could not format ( R e. Rng -> ( SubRng ` R ) C_ ~P B ) : No typesetting found for |- ( R e. Rng -> ( SubRng ` R ) C_ ~P B ) with typecode |-
7	1	subrngid	Could not format ( R e. Rng -> B e. ( SubRng ` R ) ) : No typesetting found for |- ( R e. Rng -> B e. ( SubRng ` R ) ) with typecode |-
8		subrngint	Could not format ( ( a C_ ( SubRng ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRng ` R ) ) : No typesetting found for |- ( ( a C_ ( SubRng ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRng ` R ) ) with typecode |-
9	8	3adant1	Could not format ( ( R e. Rng /\ a C_ ( SubRng ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRng ` R ) ) : No typesetting found for |- ( ( R e. Rng /\ a C_ ( SubRng ` R ) /\ a =/= (/) ) -> |^| a e. ( SubRng ` R ) ) with typecode |-
10	6 7 9	ismred	Could not format ( R e. Rng -> ( SubRng ` R ) e. ( Moore ` B ) ) : No typesetting found for |- ( R e. Rng -> ( SubRng ` R ) e. ( Moore ` B ) ) with typecode |-