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	|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B )

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	|- B = ( Base ` R )
2	1	ismxidl	|- ( 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 ) ) ) ) )
3	2	biimpa	|- ( ( 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 ) ) ) )
4	3	simp2d	|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B )