Theorem maxidlnr

Description: A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	maxidlnr.1	|- G = ( 1st ` R )
	maxidlnr.2	|- X = ran G
Assertion	maxidlnr	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M =/= X )

Proof

Step	Hyp	Ref	Expression
1		maxidlnr.1	|- G = ( 1st ` R )
2		maxidlnr.2	|- X = ran G
3	1 2	ismaxidl	|- ( R e. RingOps -> ( M e. ( MaxIdl ` R ) <-> ( M e. ( Idl ` R ) /\ M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) ) )
4	3	biimpa	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> ( M e. ( Idl ` R ) /\ M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) )
5	4	simp2d	|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M =/= X )