Definition df-maxidl 35289

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

Step	Hyp	Ref	Expression
1		cmaxidl 35286	. 2 class MaxIdl
2		vr	. . 3 setvar 𝑟
3		crngo 35171	. . 3 class RingOps
4		vi	. . . . . . 7 setvar 𝑖
5	4	cv 1532	. . . . . 6 class 𝑖
6	2	cv 1532	. . . . . . . 8 class 𝑟
7		c1st 7686	. . . . . . . 8 class 1st
8	6, 7	cfv 6354	. . . . . . 7 class (1st ‘𝑟)
9	8	crn 5555	. . . . . 6 class ran (1st ‘𝑟)
10	5, 9	wne 3016	. . . . 5 wff 𝑖 ≠ ran (1st ‘𝑟)
11		vj	. . . . . . . . 9 setvar 𝑗
12	11	cv 1532	. . . . . . . 8 class 𝑗
13	5, 12	wss 3935	. . . . . . 7 wff 𝑖 ⊆ 𝑗
14	11, 4	weq 1960	. . . . . . . 8 wff 𝑗 = 𝑖
15	12, 9	wceq 1533	. . . . . . . 8 wff 𝑗 = ran (1st ‘𝑟)
16	14, 15	wo 843	. . . . . . 7 wff (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))
17	13, 16	wi 4	. . . . . 6 wff (𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟)))
18		cidl 35284	. . . . . . 7 class Idl
19	6, 18	cfv 6354	. . . . . 6 class (Idl‘𝑟)
20	17, 11, 19	wral 3138	. . . . 5 wff ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟)))
21	10, 20	wa 398	. . . 4 wff (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))
22	21, 4, 19	crab 3142	. . 3 class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))}
23	2, 3, 22	cmpt 5145	. 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})
24	1, 23	wceq 1533	1 wff MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})

This definition is referenced by:  maxidlval  35316