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	|- MaxIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmxidl	|- MaxIdeal
1		vr	|- r
2		crg	|- Ring
3		vi	|- i
4		clidl	|- LIdeal
5	1	cv	|- r
6	5 4	cfv	|- ( LIdeal ` r )
7	3	cv	|- i
8		cbs	|- Base
9	5 8	cfv	|- ( Base ` r )
10	7 9	wne	|- i =/= ( Base ` r )
11		vj	|- j
12	11	cv	|- j
13	7 12	wss	|- i C_ j
14	12 7	wceq	|- j = i
15	12 9	wceq	|- j = ( Base ` r )
16	14 15	wo	|- ( j = i \/ j = ( Base ` r ) )
17	13 16	wi	|- ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) )
18	17 11 6	wral	|- A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) )
19	10 18	wa	|- ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) )
20	19 3 6	crab	|- { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) }
21	1 2 20	cmpt	|- ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } )
22	0 21	wceq	|- MaxIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } )