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 = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmaxidl MaxIdl
1 vr 𝑟
2 crngo RingOps
3 vi 𝑖
4 cidl Idl
5 1 cv 𝑟
6 5 4 cfv ( Idl ‘ 𝑟 )
7 3 cv 𝑖
8 c1st 1st
9 5 8 cfv ( 1st𝑟 )
10 9 crn ran ( 1st𝑟 )
11 7 10 wne 𝑖 ≠ ran ( 1st𝑟 )
12 vj 𝑗
13 12 cv 𝑗
14 7 13 wss 𝑖𝑗
15 13 7 wceq 𝑗 = 𝑖
16 13 10 wceq 𝑗 = ran ( 1st𝑟 )
17 15 16 wo ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) )
18 14 17 wi ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) ) )
19 18 12 6 wral 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) ) )
20 11 19 wa ( 𝑖 ≠ ran ( 1st𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) ) ) )
21 20 3 6 crab { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) ) ) ) }
22 1 2 21 cmpt ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) ) ) ) } )
23 0 22 wceq MaxIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖𝑗 → ( 𝑗 = 𝑖𝑗 = ran ( 1st𝑟 ) ) ) ) } )