This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion ssmxidl ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝐼 ⊆ 𝑚 )

Proof

Step Hyp Ref Expression
1 ssmxidl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 neeq1 ⊢ ( 𝑝 = 𝐼 → ( 𝑝 ≠ 𝐵 ↔ 𝐼 ≠ 𝐵 ) )
3 sseq2 ⊢ ( 𝑝 = 𝐼 → ( 𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝐼 ) )
4 2 3 anbi12d ⊢ ( 𝑝 = 𝐼 → ( ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) ↔ ( 𝐼 ≠ 𝐵 ∧ 𝐼 ⊆ 𝐼 ) ) )
5 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
6 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → 𝐼 ≠ 𝐵 )
7 ssidd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → 𝐼 ⊆ 𝐼 )
8 6 7 jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ( 𝐼 ≠ 𝐵 ∧ 𝐼 ⊆ 𝐼 ) )
9 4 5 8 elrabd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → 𝐼 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } )
10 9 ne0d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ≠ ∅ )
11 eqid ⊢ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) }
12 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝑅 ∈ Ring )
13 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
14 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝐼 ≠ 𝐵 )
15 simpr1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } )
16 simpr2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝑧 ≠ ∅ )
17 simpr3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → [⊊] Or 𝑧 )
18 1 11 12 13 14 15 16 17 ssmxidllem ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → ∪ 𝑧 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } )
19 18 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ( ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ) )
20 19 alrimiv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ∀ 𝑧 ( ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ) )
21 fvex ⊢ ( LIdeal ‘ 𝑅 ) ∈ V
22 21 rabex ⊢ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∈ V
23 22 zornn0 ⊢ ( ( { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧 ⊆ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ) ) → ∃ 𝑚 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 )
24 10 20 23 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ∃ 𝑚 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 )
25 neeq1 ⊢ ( 𝑝 = 𝑚 → ( 𝑝 ≠ 𝐵 ↔ 𝑚 ≠ 𝐵 ) )
26 sseq2 ⊢ ( 𝑝 = 𝑚 → ( 𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑚 ) )
27 25 26 anbi12d ⊢ ( 𝑝 = 𝑚 → ( ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) ↔ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) )
28 27 elrab ⊢ ( 𝑚 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) )
29 28 anbi2i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) )
30 simpll1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → 𝑅 ∈ Ring )
31 simplrl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → 𝑚 ∈ ( LIdeal ‘ 𝑅 ) )
32 simplr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) )
33 32 simprld ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → 𝑚 ≠ 𝐵 )
34 psseq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑚 ⊊ 𝑗 ↔ 𝑚 ⊊ 𝑘 ) )
35 34 notbid ⊢ ( 𝑗 = 𝑘 → ( ¬ 𝑚 ⊊ 𝑗 ↔ ¬ 𝑚 ⊊ 𝑘 ) )
36 simp-4r ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 )
37 neeq1 ⊢ ( 𝑝 = 𝑘 → ( 𝑝 ≠ 𝐵 ↔ 𝑘 ≠ 𝐵 ) )
38 sseq2 ⊢ ( 𝑝 = 𝑘 → ( 𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑘 ) )
39 37 38 anbi12d ⊢ ( 𝑝 = 𝑘 → ( ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) ↔ ( 𝑘 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑘 ) ) )
40 simpllr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) )
41 simpr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → ¬ 𝑘 = 𝐵 )
42 41 neqned ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝑘 ≠ 𝐵 )
43 simp-5r ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) )
44 43 simprrd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝐼 ⊆ 𝑚 )
45 simplr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝑚 ⊆ 𝑘 )
46 44 45 sstrd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝐼 ⊆ 𝑘 )
47 42 46 jca ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → ( 𝑘 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑘 ) )
48 39 40 47 elrabd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝑘 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } )
49 35 36 48 rspcdva ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → ¬ 𝑚 ⊊ 𝑘 )
50 npss ⊢ ( ¬ 𝑚 ⊊ 𝑘 ↔ ( 𝑚 ⊆ 𝑘 → 𝑚 = 𝑘 ) )
51 50 biimpi ⊢ ( ¬ 𝑚 ⊊ 𝑘 → ( 𝑚 ⊆ 𝑘 → 𝑚 = 𝑘 ) )
52 49 45 51 sylc ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝑚 = 𝑘 )
53 52 equcomd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) ∧ ¬ 𝑘 = 𝐵 ) → 𝑘 = 𝑚 )
54 53 ex ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) → ( ¬ 𝑘 = 𝐵 → 𝑘 = 𝑚 ) )
55 54 orrd ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) → ( 𝑘 = 𝐵 ∨ 𝑘 = 𝑚 ) )
56 55 orcomd ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑚 ⊆ 𝑘 ) → ( 𝑘 = 𝑚 ∨ 𝑘 = 𝐵 ) )
57 56 ex ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑚 ⊆ 𝑘 → ( 𝑘 = 𝑚 ∨ 𝑘 = 𝐵 ) ) )
58 57 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑘 → ( 𝑘 = 𝑚 ∨ 𝑘 = 𝐵 ) ) )
59 1 ismxidl ⊢ ( 𝑅 ∈ Ring → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑘 → ( 𝑘 = 𝑚 ∨ 𝑘 = 𝐵 ) ) ) ) )
60 59 biimpar ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ 𝐵 ∧ ∀ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑘 → ( 𝑘 = 𝑚 ∨ 𝑘 = 𝐵 ) ) ) ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
61 30 31 33 58 60 syl13anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
62 32 simprrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → 𝐼 ⊆ 𝑚 )
63 61 62 jca ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑚 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑚 ) ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑚 ) )
64 29 63 sylanb ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) ∧ 𝑚 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑚 ) )
65 64 expl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ( ( 𝑚 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 ) → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑚 ) ) )
66 65 reximdv2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ( ∃ 𝑚 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝 ) } ¬ 𝑚 ⊊ 𝑗 → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝐼 ⊆ 𝑚 ) )
67 24 66 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝐼 ⊆ 𝑚 )