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 36474
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 36471 . 2 class MaxIdl
2 vr . . 3 setvar 𝑟
3 crngo 36356 . . 3 class RingOps
4 vi . . . . . . 7 setvar 𝑖
54cv 1541 . . . . . 6 class 𝑖
62cv 1541 . . . . . . . 8 class 𝑟
7 c1st 7920 . . . . . . . 8 class 1st
86, 7cfv 6497 . . . . . . 7 class (1st𝑟)
98crn 5635 . . . . . 6 class ran (1st𝑟)
105, 9wne 2944 . . . . 5 wff 𝑖 ≠ ran (1st𝑟)
11 vj . . . . . . . . 9 setvar 𝑗
1211cv 1541 . . . . . . . 8 class 𝑗
135, 12wss 3911 . . . . . . 7 wff 𝑖𝑗
1411, 4weq 1967 . . . . . . . 8 wff 𝑗 = 𝑖
1512, 9wceq 1542 . . . . . . . 8 wff 𝑗 = ran (1st𝑟)
1614, 15wo 846 . . . . . . 7 wff (𝑗 = 𝑖𝑗 = ran (1st𝑟))
1713, 16wi 4 . . . . . 6 wff (𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟)))
18 cidl 36469 . . . . . . 7 class Idl
196, 18cfv 6497 . . . . . 6 class (Idl‘𝑟)
2017, 11, 19wral 3065 . . . . 5 wff 𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟)))
2110, 20wa 397 . . . 4 wff (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))
2221, 4, 19crab 3408 . . 3 class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))}
232, 3, 22cmpt 5189 . 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))})
241, 23wceq 1542 1 wff MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖𝑗 → (𝑗 = 𝑖𝑗 = ran (1st𝑟))))})
Colors of variables: wff setvar class
This definition is referenced by:  maxidlval  36501
  Copyright terms: Public domain W3C validator