| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | intssuni 4970 | . . . 4
⊢ (𝐶 ≠ ∅ → ∩ 𝐶
⊆ ∪ 𝐶) | 
| 2 | 1 | 3ad2ant2 1135 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶
⊆ ∪ 𝐶) | 
| 3 |  | ssel2 3978 | . . . . . . . 8
⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (Idl‘𝑅)) | 
| 4 |  | eqid 2737 | . . . . . . . . 9
⊢
(1st ‘𝑅) = (1st ‘𝑅) | 
| 5 |  | eqid 2737 | . . . . . . . . 9
⊢ ran
(1st ‘𝑅) =
ran (1st ‘𝑅) | 
| 6 | 4, 5 | idlss 38023 | . . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st ‘𝑅)) | 
| 7 | 3, 6 | sylan2 593 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → 𝑖 ⊆ ran (1st ‘𝑅)) | 
| 8 | 7 | anassrs 467 | . . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖 ∈ 𝐶) → 𝑖 ⊆ ran (1st ‘𝑅)) | 
| 9 | 8 | ralrimiva 3146 | . . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)) | 
| 10 | 9 | 3adant2 1132 | . . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)) | 
| 11 |  | unissb 4939 | . . . 4
⊢ (∪ 𝐶
⊆ ran (1st ‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)) | 
| 12 | 10, 11 | sylibr 234 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∪ 𝐶
⊆ ran (1st ‘𝑅)) | 
| 13 | 2, 12 | sstrd 3994 | . 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶
⊆ ran (1st ‘𝑅)) | 
| 14 |  | eqid 2737 | . . . . . . . 8
⊢
(GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅)) | 
| 15 | 4, 14 | idl0cl 38025 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) →
(GId‘(1st ‘𝑅)) ∈ 𝑖) | 
| 16 | 3, 15 | sylan2 593 | . . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (GId‘(1st
‘𝑅)) ∈ 𝑖) | 
| 17 | 16 | anassrs 467 | . . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖 ∈ 𝐶) → (GId‘(1st
‘𝑅)) ∈ 𝑖) | 
| 18 | 17 | ralrimiva 3146 | . . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) | 
| 19 |  | fvex 6919 | . . . . 5
⊢
(GId‘(1st ‘𝑅)) ∈ V | 
| 20 | 19 | elint2 4953 | . . . 4
⊢
((GId‘(1st ‘𝑅)) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) | 
| 21 | 18, 20 | sylibr 234 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) →
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶) | 
| 22 | 21 | 3adant2 1132 | . 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) →
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶) | 
| 23 |  | vex 3484 | . . . . . 6
⊢ 𝑥 ∈ V | 
| 24 | 23 | elint2 4953 | . . . . 5
⊢ (𝑥 ∈ ∩ 𝐶
↔ ∀𝑖 ∈
𝐶 𝑥 ∈ 𝑖) | 
| 25 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 26 | 25 | elint2 4953 | . . . . . . . . 9
⊢ (𝑦 ∈ ∩ 𝐶
↔ ∀𝑖 ∈
𝐶 𝑦 ∈ 𝑖) | 
| 27 |  | r19.26 3111 | . . . . . . . . . . 11
⊢
(∀𝑖 ∈
𝐶 (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) ↔ (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ∧ ∀𝑖 ∈ 𝐶 𝑦 ∈ 𝑖)) | 
| 28 | 4 | idladdcl 38026 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖) | 
| 29 | 28 | ex 412 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → ((𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) | 
| 30 | 3, 29 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → ((𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) | 
| 31 | 30 | anassrs 467 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖 ∈ 𝐶) → ((𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) | 
| 32 | 31 | ralimdva 3167 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → ∀𝑖 ∈ 𝐶 (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) | 
| 33 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢ (𝑥(1st ‘𝑅)𝑦) ∈ V | 
| 34 | 33 | elint2 4953 | . . . . . . . . . . . 12
⊢ ((𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖) | 
| 35 | 32, 34 | imbitrrdi 252 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) | 
| 36 | 27, 35 | biimtrrid 243 | . . . . . . . . . 10
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ((∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ∧ ∀𝑖 ∈ 𝐶 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) | 
| 37 | 36 | expdimp 452 | . . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (∀𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) | 
| 38 | 26, 37 | biimtrid 242 | . . . . . . . 8
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (𝑦 ∈ ∩ 𝐶 → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) | 
| 39 | 38 | ralrimiv 3145 | . . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶) | 
| 40 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) | 
| 41 | 4, 40, 5 | idllmulcl 38027 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) | 
| 42 | 41 | anass1rs 655 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑥 ∈ 𝑖) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) | 
| 43 | 42 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) | 
| 44 | 43 | an32s 652 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) | 
| 45 | 3, 44 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) | 
| 46 | 45 | an4s 660 | . . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) | 
| 47 | 46 | anassrs 467 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑖 ∈ 𝐶) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) | 
| 48 | 47 | ralimdva 3167 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → ∀𝑖 ∈ 𝐶 (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) | 
| 49 | 48 | imp 406 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑖 ∈ 𝐶 (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) | 
| 50 |  | ovex 7464 | . . . . . . . . . . . 12
⊢ (𝑧(2nd ‘𝑅)𝑥) ∈ V | 
| 51 | 50 | elint2 4953 | . . . . . . . . . . 11
⊢ ((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) | 
| 52 | 49, 51 | sylibr 234 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶) | 
| 53 | 4, 40, 5 | idlrmulcl 38028 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) | 
| 54 | 53 | anass1rs 655 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑥 ∈ 𝑖) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) | 
| 55 | 54 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) | 
| 56 | 55 | an32s 652 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) | 
| 57 | 3, 56 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) | 
| 58 | 57 | an4s 660 | . . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) | 
| 59 | 58 | anassrs 467 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑖 ∈ 𝐶) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) | 
| 60 | 59 | ralimdva 3167 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → ∀𝑖 ∈ 𝐶 (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) | 
| 61 | 60 | imp 406 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑖 ∈ 𝐶 (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) | 
| 62 |  | ovex 7464 | . . . . . . . . . . . 12
⊢ (𝑥(2nd ‘𝑅)𝑧) ∈ V | 
| 63 | 62 | elint2 4953 | . . . . . . . . . . 11
⊢ ((𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) | 
| 64 | 61, 63 | sylibr 234 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶) | 
| 65 | 52, 64 | jca 511 | . . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)) | 
| 66 | 65 | an32s 652 | . . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)) | 
| 67 | 66 | ralrimiva 3146 | . . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)) | 
| 68 | 39, 67 | jca 511 | . . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))) | 
| 69 | 68 | ex 412 | . . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → (∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)))) | 
| 70 | 24, 69 | biimtrid 242 | . . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑥 ∈ ∩ 𝐶 → (∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)))) | 
| 71 | 70 | ralrimiv 3145 | . . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))) | 
| 72 | 71 | 3adant2 1132 | . 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))) | 
| 73 | 4, 40, 5, 14 | isidl 38021 | . . 3
⊢ (𝑅 ∈ RingOps → (∩ 𝐶
∈ (Idl‘𝑅) ↔
(∩ 𝐶 ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶 ∧ ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))))) | 
| 74 | 73 | 3ad2ant1 1134 | . 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∩ 𝐶
∈ (Idl‘𝑅) ↔
(∩ 𝐶 ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶 ∧ ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))))) | 
| 75 | 13, 22, 72, 74 | mpbir3and 1343 | 1
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶
∈ (Idl‘𝑅)) |