Metamath Proof Explorer

Theorem maxidlmax

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

Ref Expression
Hypotheses maxidlnr.1 
|- G = ( 1st ` R )
maxidlnr.2 
|- X = ran G
Assertion maxidlmax 
|- ( ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) /\ ( I e. ( Idl ` R ) /\ M C_ I ) ) -> ( I = M \/ I = 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 simp3d 
 |-  ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) -> A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) )
6 sseq2 
 |-  ( j = I -> ( M C_ j <-> M C_ I ) )
7 eqeq1 
 |-  ( j = I -> ( j = M <-> I = M ) )
8 eqeq1 
 |-  ( j = I -> ( j = X <-> I = X ) )
9 7 8 orbi12d 
 |-  ( j = I -> ( ( j = M \/ j = X ) <-> ( I = M \/ I = X ) ) )
10 6 9 imbi12d 
 |-  ( j = I -> ( ( M C_ j -> ( j = M \/ j = X ) ) <-> ( M C_ I -> ( I = M \/ I = X ) ) ) )
11 10 rspcva 
 |-  ( ( I e. ( Idl ` R ) /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) -> ( M C_ I -> ( I = M \/ I = X ) ) )
12 5 11 sylan2 
 |-  ( ( I e. ( Idl ` R ) /\ ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) ) -> ( M C_ I -> ( I = M \/ I = X ) ) )
13 12 ancoms 
 |-  ( ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) /\ I e. ( Idl ` R ) ) -> ( M C_ I -> ( I = M \/ I = X ) ) )
14 13 impr 
 |-  ( ( ( R e. RingOps /\ M e. ( MaxIdl ` R ) ) /\ ( I e. ( Idl ` R ) /\ M C_ I ) ) -> ( I = M \/ I = X ) )