Definition df-maxidl 38914

Description: Obsolete defintion, use df-mxidl 33967 instead. 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.) (New usage is discouraged.)

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 38911	. 2 class MaxIdl
2		vr	. . 3 setvar 𝑟
3		crngo 38796	. . 3 class RingOps
4		vi	. . . . . . 7 setvar 𝑖
5	4	cv 1569	. . . . . 6 class 𝑖
6	2	cv 1569	. . . . . . . 8 class 𝑟
7		c1st 7988	. . . . . . . 8 class 1st
8	6, 7	cfv 6531	. . . . . . 7 class (1st ‘𝑟)
9	8	crn 5652	. . . . . 6 class ran (1st ‘𝑟)
10	5, 9	wne 2956	. . . . 5 wff 𝑖 ≠ ran (1st ‘𝑟)
11		vj	. . . . . . . . 9 setvar 𝑗
12	11	cv 1569	. . . . . . . 8 class 𝑗
13	5, 12	wss 3899	. . . . . . 7 wff 𝑖 ⊆ 𝑗
14	11, 4	weq 1995	. . . . . . . 8 wff 𝑗 = 𝑖
15	12, 9	wceq 1570	. . . . . . . 8 wff 𝑗 = ran (1st ‘𝑟)
16	14, 15	wo 861	. . . . . . 7 wff (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))
17	13, 16	wi 4	. . . . . 6 wff (𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟)))
18		cidl 38909	. . . . . . 7 class Idl
19	6, 18	cfv 6531	. . . . . 6 class (Idl‘𝑟)
20	17, 11, 19	wral 3077	. . . . 5 wff ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟)))
21	10, 20	wa 401	. . . 4 wff (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))
22	21, 4, 19	crab 3413	. . 3 class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))}
23	2, 3, 22	cmpt 5186	. 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})
24	1, 23	wceq 1570	1 wff MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})

This definition is used by:  maxidlval  38941