Metamath Proof Explorer

Theorem maxidlidl

Description: A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011)

Ref Expression
Assertion maxidlidl 
|- ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M e. ( Idl ` R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
2 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
3 1 2 ismaxidl 
 |-  ( R e. RingOps -> ( M e. ( MaxIdl ` R ) <-> ( M e. ( Idl ` R ) /\ M =/= ran ( 1st ` R ) /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = ran ( 1st ` R ) ) ) ) ) )
4 3anass 
 |-  ( ( M e. ( Idl ` R ) /\ M =/= ran ( 1st ` R ) /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = ran ( 1st ` R ) ) ) ) <-> ( M e. ( Idl ` R ) /\ ( M =/= ran ( 1st ` R ) /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = ran ( 1st ` R ) ) ) ) ) )
5 3 4 bitrdi 
 |-  ( R e. RingOps -> ( M e. ( MaxIdl ` R ) <-> ( M e. ( Idl ` R ) /\ ( M =/= ran ( 1st ` R ) /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = ran ( 1st ` R ) ) ) ) ) ) )
6 5 simprbda 
 |-  ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> M e. ( Idl ` R ) )