Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-maxidl Structured version   Visualization version   GIF version

Definition df-maxidl 35408
Description: Define the class of maximal ideals of a ring 𝑅. A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.)
Assertion
Ref Expression
df-maxidl MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))})
Distinct variable group:   𝑖,𝑟,𝑗

Detailed syntax breakdown of Definition df-maxidl
StepHypRef Expression
1 cmaxidl 35405 . 2 class MaxIdl
2 vr . . 3 setvar 𝑟
3 crngo 35290 . . 3 class RingOps
4 vi . . . . . . 7 setvar 𝑖
54cv 1537 . . . . . 6 class 𝑖
62cv 1537 . . . . . . . 8 class 𝑟
7 c1st 7673 . . . . . . . 8 class 1st
86, 7cfv 6334 . . . . . . 7 class (1st𝑟)
98crn 5533 . . . . . 6 class ran (1st𝑟)
105, 9wne 3011 . . . . 5 wff 𝑖 ≠ ran (1st𝑟)
11 vj . . . . . . . . 9 setvar 𝑗
1211cv 1537 . . . . . . . 8 class 𝑗
135, 12wss 3908 . . . . . . 7 wff 𝑖𝑗
1411, 4weq 1964 . . . . . . . 8 wff 𝑗 = 𝑖
1512, 9wceq 1538 . . . . . . . 8 wff 𝑗 = ran (1st𝑟)
1614, 15wo 844 . . . . . . 7 wff (𝑗 = 𝑖𝑗 = ran (1st𝑟))
1713, 16wi 4 . . . . . 6 wff (𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟)))
18 cidl 35403 . . . . . . 7 class Idl
196, 18cfv 6334 . . . . . 6 class (Idl‘𝑟)
2017, 11, 19wral 3130 . . . . 5 wff 𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟)))
2110, 20wa 399 . . . 4 wff (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))
2221, 4, 19crab 3134 . . 3 class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))}
232, 3, 22cmpt 5122 . 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))})
241, 23wceq 1538 1 wff MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))})
Colors of variables: wff setvar class
This definition is referenced by:  maxidlval  35435
  Copyright terms: Public domain W3C validator