| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ RingOps) | 
| 2 |  | smprngpr.1 | . . . . 5
⊢ 𝐺 = (1st ‘𝑅) | 
| 3 |  | smprngpr.4 | . . . . 5
⊢ 𝑍 = (GId‘𝐺) | 
| 4 | 2, 3 | 0idl 38033 | . . . 4
⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) | 
| 5 | 4 | 3ad2ant1 1133 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (Idl‘𝑅)) | 
| 6 |  | smprngpr.2 | . . . . . . . 8
⊢ 𝐻 = (2nd ‘𝑅) | 
| 7 |  | smprngpr.3 | . . . . . . . 8
⊢ 𝑋 = ran 𝐺 | 
| 8 |  | smprngpr.5 | . . . . . . . 8
⊢ 𝑈 = (GId‘𝐻) | 
| 9 | 2, 6, 7, 3, 8 | 0rngo 38035 | . . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝑍 = 𝑈 ↔ 𝑋 = {𝑍})) | 
| 10 |  | eqcom 2743 | . . . . . . 7
⊢ (𝑈 = 𝑍 ↔ 𝑍 = 𝑈) | 
| 11 |  | eqcom 2743 | . . . . . . 7
⊢ ({𝑍} = 𝑋 ↔ 𝑋 = {𝑍}) | 
| 12 | 9, 10, 11 | 3bitr4g 314 | . . . . . 6
⊢ (𝑅 ∈ RingOps → (𝑈 = 𝑍 ↔ {𝑍} = 𝑋)) | 
| 13 | 12 | necon3bid 2984 | . . . . 5
⊢ (𝑅 ∈ RingOps → (𝑈 ≠ 𝑍 ↔ {𝑍} ≠ 𝑋)) | 
| 14 | 13 | biimpa 476 | . . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → {𝑍} ≠ 𝑋) | 
| 15 | 14 | 3adant3 1132 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ≠ 𝑋) | 
| 16 |  | df-pr 4628 | . . . . . . . 8
⊢ {{𝑍}, 𝑋} = ({{𝑍}} ∪ {𝑋}) | 
| 17 | 16 | eqeq2i 2749 | . . . . . . 7
⊢
((Idl‘𝑅) =
{{𝑍}, 𝑋} ↔ (Idl‘𝑅) = ({{𝑍}} ∪ {𝑋})) | 
| 18 |  | eleq2 2829 | . . . . . . . . 9
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑖 ∈ ({{𝑍}} ∪ {𝑋}))) | 
| 19 |  | eleq2 2829 | . . . . . . . . 9
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → (𝑗 ∈ (Idl‘𝑅) ↔ 𝑗 ∈ ({{𝑍}} ∪ {𝑋}))) | 
| 20 | 18, 19 | anbi12d 632 | . . . . . . . 8
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})))) | 
| 21 |  | elun 4152 | . . . . . . . . . 10
⊢ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋})) | 
| 22 |  | velsn 4641 | . . . . . . . . . . 11
⊢ (𝑖 ∈ {{𝑍}} ↔ 𝑖 = {𝑍}) | 
| 23 |  | velsn 4641 | . . . . . . . . . . 11
⊢ (𝑖 ∈ {𝑋} ↔ 𝑖 = 𝑋) | 
| 24 | 22, 23 | orbi12i 914 | . . . . . . . . . 10
⊢ ((𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)) | 
| 25 | 21, 24 | bitri 275 | . . . . . . . . 9
⊢ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)) | 
| 26 |  | elun 4152 | . . . . . . . . . 10
⊢ (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋})) | 
| 27 |  | velsn 4641 | . . . . . . . . . . 11
⊢ (𝑗 ∈ {{𝑍}} ↔ 𝑗 = {𝑍}) | 
| 28 |  | velsn 4641 | . . . . . . . . . . 11
⊢ (𝑗 ∈ {𝑋} ↔ 𝑗 = 𝑋) | 
| 29 | 27, 28 | orbi12i 914 | . . . . . . . . . 10
⊢ ((𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) | 
| 30 | 26, 29 | bitri 275 | . . . . . . . . 9
⊢ (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) | 
| 31 | 25, 30 | anbi12i 628 | . . . . . . . 8
⊢ ((𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))) | 
| 32 | 20, 31 | bitrdi 287 | . . . . . . 7
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))) | 
| 33 | 17, 32 | sylbi 217 | . . . . . 6
⊢
((Idl‘𝑅) =
{{𝑍}, 𝑋} → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))) | 
| 34 | 33 | 3ad2ant3 1135 | . . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))) | 
| 35 |  | eqimss 4041 | . . . . . . . . . . 11
⊢ (𝑖 = {𝑍} → 𝑖 ⊆ {𝑍}) | 
| 36 | 35 | orcd 873 | . . . . . . . . . 10
⊢ (𝑖 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) | 
| 37 | 36 | adantr 480 | . . . . . . . . 9
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) | 
| 38 | 37 | a1d 25 | . . . . . . . 8
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) | 
| 39 | 38 | a1i 11 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 40 |  | eqimss 4041 | . . . . . . . . . . 11
⊢ (𝑗 = {𝑍} → 𝑗 ⊆ {𝑍}) | 
| 41 | 40 | olcd 874 | . . . . . . . . . 10
⊢ (𝑗 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) | 
| 42 | 41 | adantl 481 | . . . . . . . . 9
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) | 
| 43 | 42 | a1d 25 | . . . . . . . 8
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) | 
| 44 | 43 | a1i 11 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 45 | 36 | adantr 480 | . . . . . . . . 9
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) | 
| 46 | 45 | a1d 25 | . . . . . . . 8
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) | 
| 47 | 46 | a1i 11 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 48 | 2 | rneqi 5947 | . . . . . . . . . . . . . 14
⊢ ran 𝐺 = ran (1st
‘𝑅) | 
| 49 | 7, 48 | eqtri 2764 | . . . . . . . . . . . . 13
⊢ 𝑋 = ran (1st
‘𝑅) | 
| 50 | 49, 6, 8 | rngo1cl 37947 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → 𝑈 ∈ 𝑋) | 
| 52 | 6, 49, 8 | rngolidm 37945 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋) → (𝑈𝐻𝑈) = 𝑈) | 
| 53 | 50, 52 | mpdan 687 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ RingOps → (𝑈𝐻𝑈) = 𝑈) | 
| 54 | 53 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ∈ {𝑍})) | 
| 55 | 8 | fvexi 6919 | . . . . . . . . . . . . . . 15
⊢ 𝑈 ∈ V | 
| 56 | 55 | elsn 4640 | . . . . . . . . . . . . . 14
⊢ (𝑈 ∈ {𝑍} ↔ 𝑈 = 𝑍) | 
| 57 | 54, 56 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 = 𝑍)) | 
| 58 | 57 | necon3bbid 2977 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ RingOps → (¬
(𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ≠ 𝑍)) | 
| 59 | 58 | biimpar 477 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ¬ (𝑈𝐻𝑈) ∈ {𝑍}) | 
| 60 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑈 → (𝑥𝐻𝑦) = (𝑈𝐻𝑦)) | 
| 61 | 60 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑈 → ((𝑥𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑦) ∈ {𝑍})) | 
| 62 | 61 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑈 → (¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑦) ∈ {𝑍})) | 
| 63 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑈 → (𝑈𝐻𝑦) = (𝑈𝐻𝑈)) | 
| 64 | 63 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑈 → ((𝑈𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑈) ∈ {𝑍})) | 
| 65 | 64 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑈 → (¬ (𝑈𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑈) ∈ {𝑍})) | 
| 66 | 62, 65 | rspc2ev 3634 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑋 ∧ 𝑈 ∈ 𝑋 ∧ ¬ (𝑈𝐻𝑈) ∈ {𝑍}) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍}) | 
| 67 | 51, 51, 59, 66 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍}) | 
| 68 |  | rexnal2 3134 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍}) | 
| 69 | 67, 68 | sylib 218 | . . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍}) | 
| 70 | 69 | pm2.21d 121 | . . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) | 
| 71 |  | raleq 3322 | . . . . . . . . . 10
⊢ (𝑖 = 𝑋 → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍})) | 
| 72 |  | raleq 3322 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑋 → (∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})) | 
| 73 | 72 | ralbidv 3177 | . . . . . . . . . 10
⊢ (𝑗 = 𝑋 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})) | 
| 74 | 71, 73 | sylan9bb 509 | . . . . . . . . 9
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})) | 
| 75 | 74 | imbi1d 341 | . . . . . . . 8
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → ((∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) ↔ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 76 | 70, 75 | syl5ibrcom 247 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 77 | 39, 44, 47, 76 | ccased 1038 | . . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 78 | 77 | 3adant3 1132 | . . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 79 | 34, 78 | sylbid 240 | . . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) | 
| 80 | 79 | ralrimivv 3199 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) | 
| 81 | 2, 6, 7 | ispridl 38042 | . . . 4
⊢ (𝑅 ∈ RingOps → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))) | 
| 82 | 81 | 3ad2ant1 1133 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))) | 
| 83 | 5, 15, 80, 82 | mpbir3and 1342 | . 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (PrIdl‘𝑅)) | 
| 84 | 2, 3 | isprrngo 38058 | . 2
⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) | 
| 85 | 1, 83, 84 | sylanbrc 583 | 1
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing) |