Metamath Proof Explorer


Theorem mxidlnr

Description: A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 B = Base R
Assertion mxidlnr Could not format assertion : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) with typecode |-

Proof

Step Hyp Ref Expression
1 mxidlval.1 B = Base R
2 1 ismxidl Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) with typecode |-
3 2 biimpa Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) with typecode |-
4 3 simp2d Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) with typecode |-