This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) } )