Definition df-mxidl

Description: Define the class of maximal ideals of a ring R . A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

	Ref	Expression
Assertion	df-mxidl	Could not format assertion : 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 |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmxidl	Could not format MaxIdeal : No typesetting found for class MaxIdeal with typecode class
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		vi	$$setvari$$
4		clidl	$$class\mathrm{LIdeal}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class\mathrm{LIdeal}\left(r\right)$$
7	3	cv	$$setvari$$
8		cbs	$$class\mathrm{Base}$$
9	5 8	cfv	$$class{\mathrm{Base}}_r$$
10	7 9	wne	$$wffi\ne {\mathrm{Base}}_r$$
11		vj	$$setvarj$$
12	11	cv	$$setvarj$$
13	7 12	wss	$$wffi\subseteq j$$
14	12 7	wceq	$$wffj=i$$
15	12 9	wceq	$$wffj={\mathrm{Base}}_r$$
16	14 15	wo	$$wff\left(j=i\vee j={\mathrm{Base}}_r\right)$$
17	13 16	wi	$$wff\left(i\subseteq j\to \left(j=i\vee j={\mathrm{Base}}_r\right)\right)$$
18	17 11 6	wral	$$wff\forall j\in \mathrm{LIdeal}\left(r\right)\left(i\subseteq j\to \left(j=i\vee j={\mathrm{Base}}_r\right)\right)$$
19	10 18	wa	$$wff\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)$$
20	19 3 6	crab	$$class\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\}$$
21	1 2 20	cmpt	$$class\left(r\in \mathrm{Ring}⟼\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\}\right)$$
22	0 21	wceq	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 wff 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 wff