| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0idl.1 | . . . 4
⊢ 𝐺 = (1st ‘𝑅) | 
| 2 |  | eqid 2737 | . . . 4
⊢ ran 𝐺 = ran 𝐺 | 
| 3 |  | 0idl.2 | . . . 4
⊢ 𝑍 = (GId‘𝐺) | 
| 4 | 1, 2, 3 | rngo0cl 37926 | . . 3
⊢ (𝑅 ∈ RingOps → 𝑍 ∈ ran 𝐺) | 
| 5 | 4 | snssd 4809 | . 2
⊢ (𝑅 ∈ RingOps → {𝑍} ⊆ ran 𝐺) | 
| 6 | 3 | fvexi 6920 | . . . 4
⊢ 𝑍 ∈ V | 
| 7 | 6 | snid 4662 | . . 3
⊢ 𝑍 ∈ {𝑍} | 
| 8 | 7 | a1i 11 | . 2
⊢ (𝑅 ∈ RingOps → 𝑍 ∈ {𝑍}) | 
| 9 |  | velsn 4642 | . . . 4
⊢ (𝑥 ∈ {𝑍} ↔ 𝑥 = 𝑍) | 
| 10 |  | velsn 4642 | . . . . . . . 8
⊢ (𝑦 ∈ {𝑍} ↔ 𝑦 = 𝑍) | 
| 11 | 1, 2, 3 | rngo0rid 37927 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑍 ∈ ran 𝐺) → (𝑍𝐺𝑍) = 𝑍) | 
| 12 | 4, 11 | mpdan 687 | . . . . . . . . . 10
⊢ (𝑅 ∈ RingOps → (𝑍𝐺𝑍) = 𝑍) | 
| 13 |  | ovex 7464 | . . . . . . . . . . 11
⊢ (𝑍𝐺𝑍) ∈ V | 
| 14 | 13 | elsn 4641 | . . . . . . . . . 10
⊢ ((𝑍𝐺𝑍) ∈ {𝑍} ↔ (𝑍𝐺𝑍) = 𝑍) | 
| 15 | 12, 14 | sylibr 234 | . . . . . . . . 9
⊢ (𝑅 ∈ RingOps → (𝑍𝐺𝑍) ∈ {𝑍}) | 
| 16 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑦 = 𝑍 → (𝑍𝐺𝑦) = (𝑍𝐺𝑍)) | 
| 17 | 16 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑦 = 𝑍 → ((𝑍𝐺𝑦) ∈ {𝑍} ↔ (𝑍𝐺𝑍) ∈ {𝑍})) | 
| 18 | 15, 17 | syl5ibrcom 247 | . . . . . . . 8
⊢ (𝑅 ∈ RingOps → (𝑦 = 𝑍 → (𝑍𝐺𝑦) ∈ {𝑍})) | 
| 19 | 10, 18 | biimtrid 242 | . . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝑦 ∈ {𝑍} → (𝑍𝐺𝑦) ∈ {𝑍})) | 
| 20 | 19 | ralrimiv 3145 | . . . . . 6
⊢ (𝑅 ∈ RingOps →
∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍}) | 
| 21 |  | eqid 2737 | . . . . . . . . . 10
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) | 
| 22 | 3, 2, 1, 21 | rngorz 37930 | . . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑧(2nd ‘𝑅)𝑍) = 𝑍) | 
| 23 |  | ovex 7464 | . . . . . . . . . 10
⊢ (𝑧(2nd ‘𝑅)𝑍) ∈ V | 
| 24 | 23 | elsn 4641 | . . . . . . . . 9
⊢ ((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ↔ (𝑧(2nd ‘𝑅)𝑍) = 𝑍) | 
| 25 | 22, 24 | sylibr 234 | . . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍}) | 
| 26 | 3, 2, 1, 21 | rngolz 37929 | . . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑍(2nd ‘𝑅)𝑧) = 𝑍) | 
| 27 |  | ovex 7464 | . . . . . . . . . 10
⊢ (𝑍(2nd ‘𝑅)𝑧) ∈ V | 
| 28 | 27 | elsn 4641 | . . . . . . . . 9
⊢ ((𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍} ↔ (𝑍(2nd ‘𝑅)𝑧) = 𝑍) | 
| 29 | 26, 28 | sylibr 234 | . . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}) | 
| 30 | 25, 29 | jca 511 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → ((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})) | 
| 31 | 30 | ralrimiva 3146 | . . . . . 6
⊢ (𝑅 ∈ RingOps →
∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})) | 
| 32 | 20, 31 | jca 511 | . . . . 5
⊢ (𝑅 ∈ RingOps →
(∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}))) | 
| 33 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑥 = 𝑍 → (𝑥𝐺𝑦) = (𝑍𝐺𝑦)) | 
| 34 | 33 | eleq1d 2826 | . . . . . . 7
⊢ (𝑥 = 𝑍 → ((𝑥𝐺𝑦) ∈ {𝑍} ↔ (𝑍𝐺𝑦) ∈ {𝑍})) | 
| 35 | 34 | ralbidv 3178 | . . . . . 6
⊢ (𝑥 = 𝑍 → (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ↔ ∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍})) | 
| 36 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑍 → (𝑧(2nd ‘𝑅)𝑥) = (𝑧(2nd ‘𝑅)𝑍)) | 
| 37 | 36 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑥 = 𝑍 → ((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ↔ (𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍})) | 
| 38 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑥 = 𝑍 → (𝑥(2nd ‘𝑅)𝑧) = (𝑍(2nd ‘𝑅)𝑧)) | 
| 39 | 38 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑥 = 𝑍 → ((𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍} ↔ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})) | 
| 40 | 37, 39 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = 𝑍 → (((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}))) | 
| 41 | 40 | ralbidv 3178 | . . . . . 6
⊢ (𝑥 = 𝑍 → (∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}) ↔ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}))) | 
| 42 | 35, 41 | anbi12d 632 | . . . . 5
⊢ (𝑥 = 𝑍 → ((∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍})) ↔ (∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})))) | 
| 43 | 32, 42 | syl5ibrcom 247 | . . . 4
⊢ (𝑅 ∈ RingOps → (𝑥 = 𝑍 → (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍})))) | 
| 44 | 9, 43 | biimtrid 242 | . . 3
⊢ (𝑅 ∈ RingOps → (𝑥 ∈ {𝑍} → (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍})))) | 
| 45 | 44 | ralrimiv 3145 | . 2
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ {𝑍} (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}))) | 
| 46 | 1, 21, 2, 3 | isidl 38021 | . 2
⊢ (𝑅 ∈ RingOps → ({𝑍} ∈ (Idl‘𝑅) ↔ ({𝑍} ⊆ ran 𝐺 ∧ 𝑍 ∈ {𝑍} ∧ ∀𝑥 ∈ {𝑍} (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}))))) | 
| 47 | 5, 8, 45, 46 | mpbir3and 1343 | 1
⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) |