Definition df-pridl 36148

Description: Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see ispridl2 36175 and ispridlc 36207. (Contributed by Jeff Madsen, 10-Jun-2010.)

Assertion

Ref	Expression
df-pridl	⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})

Distinct variable group:   𝑖,𝑟,𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-pridl

Step	Hyp	Ref	Expression
1		cpridl 36145	. 2 class PrIdl
2		vr	. . 3 setvar 𝑟
3		crngo 36031	. . 3 class RingOps
4		vi	. . . . . . 7 setvar 𝑖
5	4	cv 1540	. . . . . 6 class 𝑖
6	2	cv 1540	. . . . . . . 8 class 𝑟
7		c1st 7815	. . . . . . . 8 class 1st
8	6, 7	cfv 6430	. . . . . . 7 class (1st ‘𝑟)
9	8	crn 5589	. . . . . 6 class ran (1st ‘𝑟)
10	5, 9	wne 2944	. . . . 5 wff 𝑖 ≠ ran (1st ‘𝑟)
11		vx	. . . . . . . . . . . . 13 setvar 𝑥
12	11	cv 1540	. . . . . . . . . . . 12 class 𝑥
13		vy	. . . . . . . . . . . . 13 setvar 𝑦
14	13	cv 1540	. . . . . . . . . . . 12 class 𝑦
15		c2nd 7816	. . . . . . . . . . . . 13 class 2nd
16	6, 15	cfv 6430	. . . . . . . . . . . 12 class (2nd ‘𝑟)
17	12, 14, 16	co 7268	. . . . . . . . . . 11 class (𝑥(2nd ‘𝑟)𝑦)
18	17, 5	wcel 2109	. . . . . . . . . 10 wff (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖
19		vb	. . . . . . . . . . 11 setvar 𝑏
20	19	cv 1540	. . . . . . . . . 10 class 𝑏
21	18, 13, 20	wral 3065	. . . . . . . . 9 wff ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖
22		va	. . . . . . . . . 10 setvar 𝑎
23	22	cv 1540	. . . . . . . . 9 class 𝑎
24	21, 11, 23	wral 3065	. . . . . . . 8 wff ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖
25	23, 5	wss 3891	. . . . . . . . 9 wff 𝑎 ⊆ 𝑖
26	20, 5	wss 3891	. . . . . . . . 9 wff 𝑏 ⊆ 𝑖
27	25, 26	wo 843	. . . . . . . 8 wff (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)
28	24, 27	wi 4	. . . . . . 7 wff (∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
29		cidl 36144	. . . . . . . 8 class Idl
30	6, 29	cfv 6430	. . . . . . 7 class (Idl‘𝑟)
31	28, 19, 30	wral 3065	. . . . . 6 wff ∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
32	31, 22, 30	wral 3065	. . . . 5 wff ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))
33	10, 32	wa 395	. . . 4 wff (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))
34	33, 4, 30	crab 3069	. . 3 class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}
35	2, 3, 34	cmpt 5161	. 2 class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})
36	1, 35	wceq 1541	1 wff PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))})

This definition is referenced by:  pridlval  36170