Theorem mxidlval

Description: The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

	Ref	Expression
Hypothesis	mxidlval.1	$$⊢B={\mathrm{Base}}_R$$
Assertion	mxidlval	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	$$⊢B={\mathrm{Base}}_R$$
2		fveq2	$$⊢r=R\to \mathrm{LIdeal}\left(r\right)=\mathrm{LIdeal}\left(R\right)$$
3		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
4	3 1	syl6eqr	$$⊢r=R\to {\mathrm{Base}}_r=B$$
5	4	neeq2d	$$⊢r=R\to \left(i\ne {\mathrm{Base}}_r\leftrightarrow i\ne B\right)$$
6	4	eqeq2d	$$⊢r=R\to \left(j={\mathrm{Base}}_r\leftrightarrow j=B\right)$$
7	6	orbi2d	$$⊢r=R\to \left(\left(j=i\vee j={\mathrm{Base}}_r\right)\leftrightarrow \left(j=i\vee j=B\right)\right)$$
8	7	imbi2d	$$⊢r=R\to \left(\left(i\subseteq j\to \left(j=i\vee j={\mathrm{Base}}_r\right)\right)\leftrightarrow \left(i\subseteq j\to \left(j=i\vee j=B\right)\right)\right)$$
9	2 8	raleqbidv	$$⊢r=R\to \left(\forall j\in \mathrm{LIdeal}\left(r\right)\left(i\subseteq j\to \left(j=i\vee j={\mathrm{Base}}_r\right)\right)\leftrightarrow \forall j\in \mathrm{LIdeal}\left(R\right)\left(i\subseteq j\to \left(j=i\vee j=B\right)\right)\right)$$
10	5 9	anbi12d	$$⊢r=R\to \left(\left(i\ne {\mathrm{Base}}_r\wedge \forall j\in \mathrm{LIdeal}\left(r\right)\left(i\subseteq j\to \left(j=i\vee j={\mathrm{Base}}_r\right)\right)\right)\leftrightarrow \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)$$
11	2 10	rabeqbidv	$$⊢r=R\to \left\{i\in \mathrm{LIdeal}\left(r\right)|\left(i\ne {\mathrm{Base}}_r\wedge \forall j\in \mathrm{LIdeal}\left(r\right)\left(i\subseteq j\to \left(j=i\vee j={\mathrm{Base}}_r\right)\right)\right)\right\}=\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\}$$
12		df-mxidl	Could not format MaxIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } ) : No typesetting found for |- MaxIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } ) with typecode |-
13		fvex	$$⊢\mathrm{LIdeal}\left(R\right)\in \mathrm{V}$$
14	13	rabex	$$⊢\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\}\in \mathrm{V}$$
15	11 12 14	fvmpt	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 |-