Definition df-maxidl 36097

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 36094	. 2 class MaxIdl
2		vr	. . 3 setvar 𝑟
3		crngo 35979	. . 3 class RingOps
4		vi	. . . . . . 7 setvar 𝑖
5	4	cv 1538	. . . . . 6 class 𝑖
6	2	cv 1538	. . . . . . . 8 class 𝑟
7		c1st 7802	. . . . . . . 8 class 1st
8	6, 7	cfv 6418	. . . . . . 7 class (1st ‘𝑟)
9	8	crn 5581	. . . . . 6 class ran (1st ‘𝑟)
10	5, 9	wne 2942	. . . . 5 wff 𝑖 ≠ ran (1st ‘𝑟)
11		vj	. . . . . . . . 9 setvar 𝑗
12	11	cv 1538	. . . . . . . 8 class 𝑗
13	5, 12	wss 3883	. . . . . . 7 wff 𝑖 ⊆ 𝑗
14	11, 4	weq 1967	. . . . . . . 8 wff 𝑗 = 𝑖
15	12, 9	wceq 1539	. . . . . . . 8 wff 𝑗 = ran (1st ‘𝑟)
16	14, 15	wo 843	. . . . . . 7 wff (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))
17	13, 16	wi 4	. . . . . 6 wff (𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟)))
18		cidl 36092	. . . . . . 7 class Idl
19	6, 18	cfv 6418	. . . . . 6 class (Idl‘𝑟)
20	17, 11, 19	wral 3063	. . . . 5 wff ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟)))
21	10, 20	wa 395	. . . 4 wff (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))
22	21, 4, 19	crab 3067	. . 3 class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))}
23	2, 3, 22	cmpt 5153	. 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})
24	1, 23	wceq 1539	1 wff MaxIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1st ‘𝑟))))})

This definition is referenced by:  maxidlval  36124