| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . 3
⊢ (𝑟 = 𝑅 → (Idl‘𝑟) = (Idl‘𝑅)) | 
| 2 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑟 = 𝑅 → (1st ‘𝑟) = (1st ‘𝑅)) | 
| 3 |  | pridlval.1 | . . . . . . . 8
⊢ 𝐺 = (1st ‘𝑅) | 
| 4 | 2, 3 | eqtr4di 2794 | . . . . . . 7
⊢ (𝑟 = 𝑅 → (1st ‘𝑟) = 𝐺) | 
| 5 | 4 | rneqd 5948 | . . . . . 6
⊢ (𝑟 = 𝑅 → ran (1st ‘𝑟) = ran 𝐺) | 
| 6 |  | pridlval.3 | . . . . . 6
⊢ 𝑋 = ran 𝐺 | 
| 7 | 5, 6 | eqtr4di 2794 | . . . . 5
⊢ (𝑟 = 𝑅 → ran (1st ‘𝑟) = 𝑋) | 
| 8 | 7 | neeq2d 3000 | . . . 4
⊢ (𝑟 = 𝑅 → (𝑖 ≠ ran (1st ‘𝑟) ↔ 𝑖 ≠ 𝑋)) | 
| 9 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (2nd ‘𝑟) = (2nd ‘𝑅)) | 
| 10 |  | pridlval.2 | . . . . . . . . . . 11
⊢ 𝐻 = (2nd ‘𝑅) | 
| 11 | 9, 10 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (2nd ‘𝑟) = 𝐻) | 
| 12 | 11 | oveqd 7449 | . . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑥(2nd ‘𝑟)𝑦) = (𝑥𝐻𝑦)) | 
| 13 | 12 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑟 = 𝑅 → ((𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 ↔ (𝑥𝐻𝑦) ∈ 𝑖)) | 
| 14 | 13 | 2ralbidv 3220 | . . . . . . 7
⊢ (𝑟 = 𝑅 → (∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 ↔ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖)) | 
| 15 | 14 | imbi1d 341 | . . . . . 6
⊢ (𝑟 = 𝑅 → ((∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)) ↔ (∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))) | 
| 16 | 1, 15 | raleqbidv 3345 | . . . . 5
⊢ (𝑟 = 𝑅 → (∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)) ↔ ∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))) | 
| 17 | 1, 16 | raleqbidv 3345 | . . . 4
⊢ (𝑟 = 𝑅 → (∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)) ↔ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))) | 
| 18 | 8, 17 | anbi12d 632 | . . 3
⊢ (𝑟 = 𝑅 → ((𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))) ↔ (𝑖 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖))))) | 
| 19 | 1, 18 | rabeqbidv 3454 | . 2
⊢ (𝑟 = 𝑅 → {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))} = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | 
| 20 |  | df-pridl 38019 | . 2
⊢ PrIdl =
(𝑟 ∈ RingOps ↦
{𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | 
| 21 |  | fvex 6918 | . . 3
⊢
(Idl‘𝑅) ∈
V | 
| 22 | 21 | rabex 5338 | . 2
⊢ {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))} ∈ V | 
| 23 | 19, 20, 22 | fvmpt 7015 | 1
⊢ (𝑅 ∈ RingOps →
(PrIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) |