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 ‘ 𝑅 ) 𝐼 ⊆ 𝑚 )