Step | Hyp | Ref
| Expression |
1 | | intssuni 4881 |
. . . 4
⊢ (𝐶 ≠ ∅ → ∩ 𝐶
⊆ ∪ 𝐶) |
2 | 1 | 3ad2ant2 1136 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶
⊆ ∪ 𝐶) |
3 | | ssel2 3895 |
. . . . . . . 8
⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (Idl‘𝑅)) |
4 | | eqid 2737 |
. . . . . . . . 9
⊢
(1st ‘𝑅) = (1st ‘𝑅) |
5 | | eqid 2737 |
. . . . . . . . 9
⊢ ran
(1st ‘𝑅) =
ran (1st ‘𝑅) |
6 | 4, 5 | idlss 35911 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st ‘𝑅)) |
7 | 3, 6 | sylan2 596 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → 𝑖 ⊆ ran (1st ‘𝑅)) |
8 | 7 | anassrs 471 |
. . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖 ∈ 𝐶) → 𝑖 ⊆ ran (1st ‘𝑅)) |
9 | 8 | ralrimiva 3105 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)) |
10 | 9 | 3adant2 1133 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)) |
11 | | unissb 4853 |
. . . 4
⊢ (∪ 𝐶
⊆ ran (1st ‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)) |
12 | 10, 11 | sylibr 237 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∪ 𝐶
⊆ ran (1st ‘𝑅)) |
13 | 2, 12 | sstrd 3911 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶
⊆ ran (1st ‘𝑅)) |
14 | | eqid 2737 |
. . . . . . . 8
⊢
(GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅)) |
15 | 4, 14 | idl0cl 35913 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) →
(GId‘(1st ‘𝑅)) ∈ 𝑖) |
16 | 3, 15 | sylan2 596 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (GId‘(1st
‘𝑅)) ∈ 𝑖) |
17 | 16 | anassrs 471 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖 ∈ 𝐶) → (GId‘(1st
‘𝑅)) ∈ 𝑖) |
18 | 17 | ralrimiva 3105 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) |
19 | | fvex 6730 |
. . . . 5
⊢
(GId‘(1st ‘𝑅)) ∈ V |
20 | 19 | elint2 4866 |
. . . 4
⊢
((GId‘(1st ‘𝑅)) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) |
21 | 18, 20 | sylibr 237 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) →
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶) |
22 | 21 | 3adant2 1133 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) →
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶) |
23 | | vex 3412 |
. . . . . 6
⊢ 𝑥 ∈ V |
24 | 23 | elint2 4866 |
. . . . 5
⊢ (𝑥 ∈ ∩ 𝐶
↔ ∀𝑖 ∈
𝐶 𝑥 ∈ 𝑖) |
25 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
26 | 25 | elint2 4866 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∩ 𝐶
↔ ∀𝑖 ∈
𝐶 𝑦 ∈ 𝑖) |
27 | | r19.26 3092 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
𝐶 (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) ↔ (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ∧ ∀𝑖 ∈ 𝐶 𝑦 ∈ 𝑖)) |
28 | 4 | idladdcl 35914 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖) |
29 | 28 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → ((𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) |
30 | 3, 29 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → ((𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) |
31 | 30 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖 ∈ 𝐶) → ((𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) |
32 | 31 | ralimdva 3100 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → ∀𝑖 ∈ 𝐶 (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)) |
33 | | ovex 7246 |
. . . . . . . . . . . . 13
⊢ (𝑥(1st ‘𝑅)𝑦) ∈ V |
34 | 33 | elint2 4866 |
. . . . . . . . . . . 12
⊢ ((𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖) |
35 | 32, 34 | syl6ibr 255 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) |
36 | 27, 35 | syl5bir 246 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ((∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ∧ ∀𝑖 ∈ 𝐶 𝑦 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) |
37 | 36 | expdimp 456 |
. . . . . . . . 9
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (∀𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) |
38 | 26, 37 | syl5bi 245 |
. . . . . . . 8
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (𝑦 ∈ ∩ 𝐶 → (𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶)) |
39 | 38 | ralrimiv 3104 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶) |
40 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) |
41 | 4, 40, 5 | idllmulcl 35915 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) |
42 | 41 | anass1rs 655 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑥 ∈ 𝑖) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) |
43 | 42 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) |
44 | 43 | an32s 652 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) |
45 | 3, 44 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) |
46 | 45 | an4s 660 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) |
47 | 46 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑖 ∈ 𝐶) → (𝑥 ∈ 𝑖 → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) |
48 | 47 | ralimdva 3100 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → ∀𝑖 ∈ 𝐶 (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖)) |
49 | 48 | imp 410 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑖 ∈ 𝐶 (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) |
50 | | ovex 7246 |
. . . . . . . . . . . 12
⊢ (𝑧(2nd ‘𝑅)𝑥) ∈ V |
51 | 50 | elint2 4866 |
. . . . . . . . . . 11
⊢ ((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑖) |
52 | 49, 51 | sylibr 237 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶) |
53 | 4, 40, 5 | idlrmulcl 35916 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) |
54 | 53 | anass1rs 655 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑥 ∈ 𝑖) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) |
55 | 54 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) |
56 | 55 | an32s 652 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) |
57 | 3, 56 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st
‘𝑅)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) |
58 | 57 | an4s 660 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑧 ∈ ran (1st ‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) |
59 | 58 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ 𝑖 ∈ 𝐶) → (𝑥 ∈ 𝑖 → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) |
60 | 59 | ralimdva 3100 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → ∀𝑖 ∈ 𝐶 (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖)) |
61 | 60 | imp 410 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑖 ∈ 𝐶 (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) |
62 | | ovex 7246 |
. . . . . . . . . . . 12
⊢ (𝑥(2nd ‘𝑅)𝑧) ∈ V |
63 | 62 | elint2 4866 |
. . . . . . . . . . 11
⊢ ((𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑖) |
64 | 61, 63 | sylibr 237 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶) |
65 | 52, 64 | jca 515 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)) |
66 | 65 | an32s 652 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)) |
67 | 66 | ralrimiva 3105 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)) |
68 | 39, 67 | jca 515 |
. . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖) → (∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))) |
69 | 68 | ex 416 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → (∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)))) |
70 | 24, 69 | syl5bi 245 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑥 ∈ ∩ 𝐶 → (∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶)))) |
71 | 70 | ralrimiv 3104 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))) |
72 | 71 | 3adant2 1133 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))) |
73 | 4, 40, 5, 14 | isidl 35909 |
. . 3
⊢ (𝑅 ∈ RingOps → (∩ 𝐶
∈ (Idl‘𝑅) ↔
(∩ 𝐶 ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶 ∧ ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))))) |
74 | 73 | 3ad2ant1 1135 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∩ 𝐶
∈ (Idl‘𝑅) ↔
(∩ 𝐶 ⊆ ran (1st ‘𝑅) ∧
(GId‘(1st ‘𝑅)) ∈ ∩ 𝐶 ∧ ∀𝑥 ∈ ∩ 𝐶(∀𝑦 ∈ ∩ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∩ 𝐶 ∧ ∀𝑧 ∈ ran (1st
‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∩ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∩ 𝐶))))) |
75 | 13, 22, 72, 74 | mpbir3and 1344 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶
∈ (Idl‘𝑅)) |