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	$$⊢B={\mathrm{Base}}_R$$
	mxidlmaxv.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	mxidlmaxv.3	$$⊢\phi \to M\in \mathrm{MaxIdeal}\left(R\right)$$
	mxidlmaxv.4	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
	mxidlmaxv.5	$$⊢\phi \to M\subseteq I$$
	mxidlmaxv.6	$$⊢\phi \to X\in \left(I\setminus M\right)$$
Assertion	mxidlmaxv	$$⊢\phi \to I=B$$

Proof

Step	Hyp	Ref	Expression
1		mxidlmaxv.1	$$⊢B={\mathrm{Base}}_R$$
2		mxidlmaxv.2	$$⊢\phi \to R\in \mathrm{Ring}$$
3		mxidlmaxv.3	$$⊢\phi \to M\in \mathrm{MaxIdeal}\left(R\right)$$
4		mxidlmaxv.4	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
5		mxidlmaxv.5	$$⊢\phi \to M\subseteq I$$
6		mxidlmaxv.6	$$⊢\phi \to X\in \left(I\setminus M\right)$$
7	1	mxidlmax	$$⊢\left(\left(R\in \mathrm{Ring}\wedge M\in \mathrm{MaxIdeal}\left(R\right)\right)\wedge \left(I\in \mathrm{LIdeal}\left(R\right)\wedge M\subseteq I\right)\right)\to \left(I=M\vee I=B\right)$$
8	2 3 4 5 7	syl22anc	$$⊢\phi \to \left(I=M\vee I=B\right)$$
9	6	eldifad	$$⊢\phi \to X\in I$$
10	6	eldifbd	$$⊢\phi \to \neg X\in M$$
11		nelne1	$$⊢\left(X\in I\wedge \neg X\in M\right)\to I\ne M$$
12	9 10 11	syl2anc	$$⊢\phi \to I\ne M$$
13	12	neneqd	$$⊢\phi \to \neg I=M$$
14	8 13	orcnd	$$⊢\phi \to I=B$$