Metamath Proof Explorer

Theorem ssmxidl

Description: Let R be a ring, and let I be a proper ideal of R . Then there is a maximal ideal of R containing I . (Contributed by Thierry Arnoux, 10-Apr-2024)

Ref Expression
Hypothesis ssmxidl.1 
|- B = ( Base ` R )
Assertion ssmxidl 
|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m )

Proof

Step Hyp Ref Expression
1 ssmxidl.1 
 |-  B = ( Base ` R )
2 neeq1 
 |-  ( p = I -> ( p =/= B <-> I =/= B ) )
3 sseq2 
 |-  ( p = I -> ( I C_ p <-> I C_ I ) )
4 2 3 anbi12d 
 |-  ( p = I -> ( ( p =/= B /\ I C_ p ) <-> ( I =/= B /\ I C_ I ) ) )
5 simp2 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> I e. ( LIdeal ` R ) )
6 simp3 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> I =/= B )
7 ssidd 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> I C_ I )
8 6 7 jca 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( I =/= B /\ I C_ I ) )
9 4 5 8 elrabd 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> I e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } )
10 9 ne0d 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } =/= (/) )
11 eqid 
 |-  { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } = { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) }
12 simpl1 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) ) -> R e. Ring )
13 simpl2 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) ) -> I e. ( LIdeal ` R ) )
14 simpl3 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) ) -> I =/= B )
15 simpr1 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) ) -> z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } )
16 simpr2 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) ) -> z =/= (/) )
17 simpr3 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) ) -> [C.] Or z )
18 1 11 12 13 14 15 16 17 ssmxidllem 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) ) -> U. z e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } )
19 18 ex 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) -> U. z e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } ) )
20 19 alrimiv 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> A. z ( ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) -> U. z e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } ) )
21 fvex 
 |-  ( LIdeal ` R ) e. _V
22 21 rabex 
 |-  { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } e. _V
23 22 zornn0 
 |-  ( ( { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } =/= (/) /\ A. z ( ( z C_ { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ z =/= (/) /\ [C.] Or z ) -> U. z e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } ) ) -> E. m e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j )
24 10 20 23 syl2anc 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j )
25 neeq1 
 |-  ( p = m -> ( p =/= B <-> m =/= B ) )
26 sseq2 
 |-  ( p = m -> ( I C_ p <-> I C_ m ) )
27 25 26 anbi12d 
 |-  ( p = m -> ( ( p =/= B /\ I C_ p ) <-> ( m =/= B /\ I C_ m ) ) )
28 27 elrab 
 |-  ( m e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } <-> ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) )
29 28 anbi2i 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ m e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } ) <-> ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) )
30 simpll1 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> R e. Ring )
31 simplrl 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> m e. ( LIdeal ` R ) )
32 simplr 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) )
33 32 simprld 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> m =/= B )
34 psseq2 
 |-  ( j = k -> ( m C. j <-> m C. k ) )
35 34 notbid 
 |-  ( j = k -> ( -. m C. j <-> -. m C. k ) )
36 simp-4r 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j )
37 neeq1 
 |-  ( p = k -> ( p =/= B <-> k =/= B ) )
38 sseq2 
 |-  ( p = k -> ( I C_ p <-> I C_ k ) )
39 37 38 anbi12d 
 |-  ( p = k -> ( ( p =/= B /\ I C_ p ) <-> ( k =/= B /\ I C_ k ) ) )
40 simpllr 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> k e. ( LIdeal ` R ) )
41 simpr 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> -. k = B )
42 41 neqned 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> k =/= B )
43 simp-5r 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) )
44 43 simprrd 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> I C_ m )
45 simplr 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> m C_ k )
46 44 45 sstrd 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> I C_ k )
47 42 46 jca 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> ( k =/= B /\ I C_ k ) )
48 39 40 47 elrabd 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> k e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } )
49 35 36 48 rspcdva 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> -. m C. k )
50 npss 
 |-  ( -. m C. k <-> ( m C_ k -> m = k ) )
51 50 biimpi 
 |-  ( -. m C. k -> ( m C_ k -> m = k ) )
52 49 45 51 sylc 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> m = k )
53 52 equcomd 
 |-  ( ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) /\ -. k = B ) -> k = m )
54 53 ex 
 |-  ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) -> ( -. k = B -> k = m ) )
55 54 orrd 
 |-  ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) -> ( k = B \/ k = m ) )
56 55 orcomd 
 |-  ( ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) /\ m C_ k ) -> ( k = m \/ k = B ) )
57 56 ex 
 |-  ( ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) /\ k e. ( LIdeal ` R ) ) -> ( m C_ k -> ( k = m \/ k = B ) ) )
58 57 ralrimiva 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> A. k e. ( LIdeal ` R ) ( m C_ k -> ( k = m \/ k = B ) ) )
59 1 ismxidl 
 |-  ( R e. Ring -> ( m e. ( MaxIdeal ` R ) <-> ( m e. ( LIdeal ` R ) /\ m =/= B /\ A. k e. ( LIdeal ` R ) ( m C_ k -> ( k = m \/ k = B ) ) ) ) )
60 59 biimpar 
 |-  ( ( R e. Ring /\ ( m e. ( LIdeal ` R ) /\ m =/= B /\ A. k e. ( LIdeal ` R ) ( m C_ k -> ( k = m \/ k = B ) ) ) ) -> m e. ( MaxIdeal ` R ) )
61 30 31 33 58 60 syl13anc 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> m e. ( MaxIdeal ` R ) )
62 32 simprrd 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> I C_ m )
63 61 62 jca 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) )
64 29 63 sylanb 
 |-  ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ m e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } ) /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) )
65 64 expl 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( ( m e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } /\ A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) ) )
66 65 reximdv2 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( E. m e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } A. j e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } -. m C. j -> E. m e. ( MaxIdeal ` R ) I C_ m ) )
67 24 66 mpd 
 |-  ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m )