Theorem mxidlmaxv

Description: An ideal I strictly containing a maximal ideal M is the whole ring B . (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypotheses	mxidlmaxv.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mxidlmaxv.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mxidlmaxv.3	⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
	mxidlmaxv.4	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
	mxidlmaxv.5	⊢ ( 𝜑 → 𝑀 ⊆ 𝐼 )
	mxidlmaxv.6	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ∖ 𝑀 ) )
Assertion	mxidlmaxv	⊢ ( 𝜑 → 𝐼 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mxidlmaxv.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		mxidlmaxv.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		mxidlmaxv.3	⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
4		mxidlmaxv.4	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
5		mxidlmaxv.5	⊢ ( 𝜑 → 𝑀 ⊆ 𝐼 )
6		mxidlmaxv.6	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ∖ 𝑀 ) )
7	1	mxidlmax	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ⊆ 𝐼 ) ) → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) )
8	2 3 4 5 7	syl22anc	⊢ ( 𝜑 → ( 𝐼 = 𝑀 ∨ 𝐼 = 𝐵 ) )
9	6	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
10	6	eldifbd	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑀 )
11		nelne1	⊢ ( ( 𝑋 ∈ 𝐼 ∧ ¬ 𝑋 ∈ 𝑀 ) → 𝐼 ≠ 𝑀 )
12	9 10 11	syl2anc	⊢ ( 𝜑 → 𝐼 ≠ 𝑀 )
13	12	neneqd	⊢ ( 𝜑 → ¬ 𝐼 = 𝑀 )
14	8 13	orcnd	⊢ ( 𝜑 → 𝐼 = 𝐵 )