Metamath Proof Explorer

Definition df-maxidl

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)

Ref Expression
Assertion df-maxidl 
|- MaxIdl = ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmaxidl 
 |-  MaxIdl
1 vr 
 |-  r
2 crngo 
 |-  RingOps
3 vi 
 |-  i
4 cidl 
 |-  Idl
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Idl ` r )
7 3 cv 
 |-  i
8 c1st 
 |-  1st
9 5 8 cfv 
 |-  ( 1st ` r )
10 9 crn 
 |-  ran ( 1st ` r )
11 7 10 wne 
 |-  i =/= ran ( 1st ` r )
12 vj 
 |-  j
13 12 cv 
 |-  j
14 7 13 wss 
 |-  i C_ j
15 13 7 wceq 
 |-  j = i
16 13 10 wceq 
 |-  j = ran ( 1st ` r )
17 15 16 wo 
 |-  ( j = i \/ j = ran ( 1st ` r ) )
18 14 17 wi 
 |-  ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) )
19 18 12 6 wral 
 |-  A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) )
20 11 19 wa 
 |-  ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) )
21 20 3 6 crab 
 |-  { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) }
22 1 2 21 cmpt 
 |-  ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) } )
23 0 22 wceq 
 |-  MaxIdl = ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) } )