Theorem ismxidl

Description: The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

	Ref	Expression
Hypothesis	mxidlval.1	$$⊢B={\mathrm{Base}}_R$$
Assertion	ismxidl	Could not format assertion : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	$$⊢B={\mathrm{Base}}_R$$
2	1	mxidlval	Could not format ( R e. Ring -> ( MaxIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) : No typesetting found for |- ( R e. Ring -> ( MaxIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) with typecode |-
3	2	eleq2d	Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> M e. { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) ) : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> M e. { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) ) with typecode |-
4		neeq1	$$⊢i=M\to \left(i\ne B\leftrightarrow M\ne B\right)$$
5		sseq1	$$⊢i=M\to \left(i\subseteq j\leftrightarrow M\subseteq j\right)$$
6		eqeq2	$$⊢i=M\to \left(j=i\leftrightarrow j=M\right)$$
7	6	orbi1d	$$⊢i=M\to \left(\left(j=i\vee j=B\right)\leftrightarrow \left(j=M\vee j=B\right)\right)$$
8	5 7	imbi12d	$$⊢i=M\to \left(\left(i\subseteq j\to \left(j=i\vee j=B\right)\right)\leftrightarrow \left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\right)$$
9	8	ralbidv	$$⊢i=M\to \left(\forall j\in \mathrm{LIdeal}\left(R\right)\left(i\subseteq j\to \left(j=i\vee j=B\right)\right)\leftrightarrow \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\right)$$
10	4 9	anbi12d	$$⊢i=M\to \left(\left(i\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(i\subseteq j\to \left(j=i\vee j=B\right)\right)\right)\leftrightarrow \left(M\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\right)\right)$$
11	10	elrab	$$⊢M\in \left\{i\in \mathrm{LIdeal}\left(R\right)|\left(i\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(i\subseteq j\to \left(j=i\vee j=B\right)\right)\right)\right\}\leftrightarrow \left(M\in \mathrm{LIdeal}\left(R\right)\wedge \left(M\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\right)\right)$$
12		3anass	$$⊢\left(M\in \mathrm{LIdeal}\left(R\right)\wedge M\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\right)\leftrightarrow \left(M\in \mathrm{LIdeal}\left(R\right)\wedge \left(M\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\right)\right)$$
13	11 12	bitr4i	$$⊢M\in \left\{i\in \mathrm{LIdeal}\left(R\right)|\left(i\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(i\subseteq j\to \left(j=i\vee j=B\right)\right)\right)\right\}\leftrightarrow \left(M\in \mathrm{LIdeal}\left(R\right)\wedge M\ne B\wedge \forall j\in \mathrm{LIdeal}\left(R\right)\left(M\subseteq j\to \left(j=M\vee j=B\right)\right)\right)$$
14	3 13	syl6bb	Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) with typecode |-