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 = ( Base ` R )
	mxidlmaxv.2	|- ( ph -> R e. Ring )
	mxidlmaxv.3	|- ( ph -> M e. ( MaxIdeal ` R ) )
	mxidlmaxv.4	|- ( ph -> I e. ( LIdeal ` R ) )
	mxidlmaxv.5	|- ( ph -> M C_ I )
	mxidlmaxv.6	|- ( ph -> X e. ( I \ M ) )
Assertion	mxidlmaxv	|- ( ph -> I = B )

Proof

Step	Hyp	Ref	Expression
1		mxidlmaxv.1	|- B = ( Base ` R )
2		mxidlmaxv.2	|- ( ph -> R e. Ring )
3		mxidlmaxv.3	|- ( ph -> M e. ( MaxIdeal ` R ) )
4		mxidlmaxv.4	|- ( ph -> I e. ( LIdeal ` R ) )
5		mxidlmaxv.5	|- ( ph -> M C_ I )
6		mxidlmaxv.6	|- ( ph -> X e. ( I \ M ) )
7	1	mxidlmax	|- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) /\ ( I e. ( LIdeal ` R ) /\ M C_ I ) ) -> ( I = M \/ I = B ) )
8	2 3 4 5 7	syl22anc	|- ( ph -> ( I = M \/ I = B ) )
9	6	eldifad	|- ( ph -> X e. I )
10	6	eldifbd	|- ( ph -> -. X e. M )
11		nelne1	|- ( ( X e. I /\ -. X e. M ) -> I =/= M )
12	9 10 11	syl2anc	|- ( ph -> I =/= M )
13	12	neneqd	|- ( ph -> -. I = M )
14	8 13	orcnd	|- ( ph -> I = B )