Step | Hyp | Ref
| Expression |
1 | | relxp 5150 |
. . . . . . . . 9
⊢ Rel
({𝑗} × 𝐵) |
2 | 1 | rgenw 2908 |
. . . . . . . 8
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐵) |
3 | | reliun 5162 |
. . . . . . . 8
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐵)) |
4 | 2, 3 | mpbir 220 |
. . . . . . 7
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
5 | | relcnv 5422 |
. . . . . . 7
⊢ Rel ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) |
6 | | ancom 465 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑗 ∧ 𝑦 = 𝑘) ↔ (𝑦 = 𝑘 ∧ 𝑥 = 𝑗)) |
7 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
8 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
9 | 7, 8 | opth 4871 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ (𝑥 = 𝑗 ∧ 𝑦 = 𝑘)) |
10 | 8, 7 | opth 4871 |
. . . . . . . . . . . 12
⊢
(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ↔ (𝑦 = 𝑘 ∧ 𝑥 = 𝑗)) |
11 | 6, 9, 10 | 3bitr4i 291 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉) |
12 | 11 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉)) |
13 | | fsumcom2.4 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
14 | 12, 13 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝜑 → ((〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) ↔ (〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)))) |
15 | 14 | 2exbidv 1839 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)))) |
16 | | eliunxp 5181 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
17 | 7, 8 | opelcnv 5226 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ 〈𝑦, 𝑥〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
18 | | eliunxp 5181 |
. . . . . . . . 9
⊢
(〈𝑦, 𝑥〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘∃𝑗(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
19 | | excom 2029 |
. . . . . . . . 9
⊢
(∃𝑘∃𝑗(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
20 | 17, 18, 19 | 3bitri 285 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
21 | 15, 16, 20 | 3bitr4g 302 |
. . . . . . 7
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷))) |
22 | 4, 5, 21 | eqrelrdv 5139 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
23 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑚({𝑗} × 𝐵) |
24 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑗{𝑚} |
25 | | nfcsb1v 3515 |
. . . . . . . 8
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐵 |
26 | 24, 25 | nfxp 5066 |
. . . . . . 7
⊢
Ⅎ𝑗({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) |
27 | | sneq 4135 |
. . . . . . . 8
⊢ (𝑗 = 𝑚 → {𝑗} = {𝑚}) |
28 | | csbeq1a 3508 |
. . . . . . . 8
⊢ (𝑗 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑗⦌𝐵) |
29 | 27, 28 | xpeq12d 5064 |
. . . . . . 7
⊢ (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)) |
30 | 23, 26, 29 | cbviun 4493 |
. . . . . 6
⊢ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) |
31 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑛({𝑘} × 𝐷) |
32 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑘{𝑛} |
33 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐷 |
34 | 32, 33 | nfxp 5066 |
. . . . . . . 8
⊢
Ⅎ𝑘({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
35 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → {𝑘} = {𝑛}) |
36 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → 𝐷 = ⦋𝑛 / 𝑘⦌𝐷) |
37 | 35, 36 | xpeq12d 5064 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ({𝑘} × 𝐷) = ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
38 | 31, 34, 37 | cbviun 4493 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) = ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
39 | 38 | cnveqi 5219 |
. . . . . 6
⊢ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) = ◡∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
40 | 22, 30, 39 | 3eqtr3g 2667 |
. . . . 5
⊢ (𝜑 → ∪ 𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ◡∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
41 | 40 | sumeq1d 14279 |
. . . 4
⊢ (𝜑 → Σ𝑧 ∈ ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = Σ𝑧 ∈ ◡ ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
42 | | vex 3176 |
. . . . . . . 8
⊢ 𝑛 ∈ V |
43 | | vex 3176 |
. . . . . . . 8
⊢ 𝑚 ∈ V |
44 | 42, 43 | op1std 7069 |
. . . . . . 7
⊢ (𝑤 = 〈𝑛, 𝑚〉 → (1st ‘𝑤) = 𝑛) |
45 | 44 | csbeq1d 3506 |
. . . . . 6
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
46 | 42, 43 | op2ndd 7070 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑛, 𝑚〉 → (2nd ‘𝑤) = 𝑚) |
47 | 46 | csbeq1d 3506 |
. . . . . . 7
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑚 / 𝑗⦌𝐸) |
48 | 47 | csbeq2dv 3944 |
. . . . . 6
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋𝑛 / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
49 | 45, 48 | eqtrd 2644 |
. . . . 5
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
50 | 43, 42 | op2ndd 7070 |
. . . . . . 7
⊢ (𝑧 = 〈𝑚, 𝑛〉 → (2nd ‘𝑧) = 𝑛) |
51 | 50 | csbeq1d 3506 |
. . . . . 6
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋(2nd
‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
52 | 43, 42 | op1std 7069 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑚, 𝑛〉 → (1st ‘𝑧) = 𝑚) |
53 | 52 | csbeq1d 3506 |
. . . . . . 7
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑚 / 𝑗⦌𝐸) |
54 | 53 | csbeq2dv 3944 |
. . . . . 6
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋𝑛 / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
55 | 51, 54 | eqtrd 2644 |
. . . . 5
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋(2nd
‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
56 | | fsumcom2.2 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Fin) |
57 | | snfi 7923 |
. . . . . . . 8
⊢ {𝑛} ∈ Fin |
58 | | fsumcom2.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ Fin) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐴 ∈ Fin) |
60 | 33 | nfcri 2745 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷 |
61 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) |
62 | | vsnid 4156 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑘 ∈ {𝑘} |
63 | 61, 62 | syl6eqelr 2697 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → 𝑛 ∈ {𝑘}) |
64 | 63 | biantrurd 528 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (𝑚 ∈ 𝐷 ↔ (𝑛 ∈ {𝑘} ∧ 𝑚 ∈ 𝐷))) |
65 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑛, 𝑚〉 ∈ ({𝑘} × 𝐷) ↔ (𝑛 ∈ {𝑘} ∧ 𝑚 ∈ 𝐷)) |
66 | 64, 65 | syl6rbbr 278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (〈𝑛, 𝑚〉 ∈ ({𝑘} × 𝐷) ↔ 𝑚 ∈ 𝐷)) |
67 | 36 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (𝑚 ∈ 𝐷 ↔ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) |
68 | 66, 67 | bitrd 267 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (〈𝑛, 𝑚〉 ∈ ({𝑘} × 𝐷) ↔ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) |
69 | 60, 68 | rspce 3277 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷) → ∃𝑘 ∈ 𝐶 〈𝑛, 𝑚〉 ∈ ({𝑘} × 𝐷)) |
70 | | eliun 4460 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑛, 𝑚〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘 ∈ 𝐶 〈𝑛, 𝑚〉 ∈ ({𝑘} × 𝐷)) |
71 | 69, 70 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷) → 〈𝑛, 𝑚〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
72 | 43, 42 | opelcnv 5226 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑚, 𝑛〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ 〈𝑛, 𝑚〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
73 | 71, 72 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷) → 〈𝑚, 𝑛〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 〈𝑚, 𝑛〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
75 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
76 | 74, 75 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 〈𝑚, 𝑛〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
77 | | eliun 4460 |
. . . . . . . . . . . . 13
⊢
(〈𝑚, 𝑛〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) |
78 | 76, 77 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → ∃𝑗 ∈ 𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) |
79 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) |
80 | | opelxp 5070 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) ↔ (𝑚 ∈ {𝑗} ∧ 𝑛 ∈ 𝐵)) |
81 | 79, 80 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → (𝑚 ∈ {𝑗} ∧ 𝑛 ∈ 𝐵)) |
82 | 81 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑚 ∈ {𝑗}) |
83 | | elsni 4142 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑗} → 𝑚 = 𝑗) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑚 = 𝑗) |
85 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑗 ∈ 𝐴) |
86 | 84, 85 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑚 ∈ 𝐴) |
87 | 86 | rexlimiva 3010 |
. . . . . . . . . . . 12
⊢
(∃𝑗 ∈
𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑚 ∈ 𝐴) |
88 | 78, 87 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 𝑚 ∈ 𝐴) |
89 | 88 | expr 641 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷 → 𝑚 ∈ 𝐴)) |
90 | 89 | ssrdv 3574 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋𝑛 / 𝑘⦌𝐷 ⊆ 𝐴) |
91 | | ssfi 8065 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧
⦋𝑛 / 𝑘⦌𝐷 ⊆ 𝐴) → ⦋𝑛 / 𝑘⦌𝐷 ∈ Fin) |
92 | 59, 90, 91 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋𝑛 / 𝑘⦌𝐷 ∈ Fin) |
93 | | xpfi 8116 |
. . . . . . . 8
⊢ (({𝑛} ∈ Fin ∧
⦋𝑛 / 𝑘⦌𝐷 ∈ Fin) → ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
94 | 57, 92, 93 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
95 | 94 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
96 | | iunfi 8137 |
. . . . . 6
⊢ ((𝐶 ∈ Fin ∧ ∀𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) → ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
97 | 56, 95, 96 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
98 | | reliun 5162 |
. . . . . . 7
⊢ (Rel
∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ↔ ∀𝑛 ∈ 𝐶 Rel ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
99 | | relxp 5150 |
. . . . . . . 8
⊢ Rel
({𝑛} ×
⦋𝑛 / 𝑘⦌𝐷) |
100 | 99 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ 𝐶 → Rel ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
101 | 98, 100 | mprgbir 2911 |
. . . . . 6
⊢ Rel
∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
102 | 101 | a1i 11 |
. . . . 5
⊢ (𝜑 → Rel ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
103 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
104 | | eliun 4460 |
. . . . . . . 8
⊢ (𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ↔ ∃𝑛 ∈ 𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
105 | 103, 104 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ∃𝑛 ∈ 𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
106 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (2nd ‘𝑤) ∈ ⦋𝑛 / 𝑘⦌𝐷) |
107 | 106 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈ ⦋𝑛 / 𝑘⦌𝐷) |
108 | | xp1st 7089 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (1st ‘𝑤) ∈ {𝑛}) |
109 | 108 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ {𝑛}) |
110 | | elsni 4142 |
. . . . . . . . . . 11
⊢
((1st ‘𝑤) ∈ {𝑛} → (1st ‘𝑤) = 𝑛) |
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) = 𝑛) |
112 | 111 | csbeq1d 3506 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ⦋(1st
‘𝑤) / 𝑘⦌𝐷 = ⦋𝑛 / 𝑘⦌𝐷) |
113 | 107, 112 | eleqtrrd 2691 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
114 | 113 | rexlimiva 3010 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
115 | 105, 114 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
116 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → 𝑛 ∈ 𝐶) |
117 | 111, 116 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ 𝐶) |
118 | 117 | rexlimiva 3010 |
. . . . . . . 8
⊢
(∃𝑛 ∈
𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (1st ‘𝑤) ∈ 𝐶) |
119 | 105, 118 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ 𝐶) |
120 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 𝜑) |
121 | 25 | nfcri 2745 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵 |
122 | 83 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ {𝑗} → 𝑗 = 𝑚) |
123 | 122, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ {𝑗} → 𝐵 = ⦋𝑚 / 𝑗⦌𝐵) |
124 | 123 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑗} → (𝑛 ∈ 𝐵 ↔ 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵)) |
125 | 124 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ {𝑗} ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
126 | 80, 125 | sylbi 206 |
. . . . . . . . . . . . 13
⊢
(〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
127 | 126 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ 𝐴 → (〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵)) |
128 | 121, 127 | rexlimi 3006 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
129 | 78, 128 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
130 | | fsumcom2.5 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐸 ∈ ℂ) |
131 | 130 | ralrimivva 2954 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ) |
132 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐸 |
133 | 132 | nfel1 2765 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ |
134 | 25, 133 | nfral 2929 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ |
135 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑚 → 𝐸 = ⦋𝑚 / 𝑗⦌𝐸) |
136 | 135 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑚 → (𝐸 ∈ ℂ ↔ ⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
137 | 28, 136 | raleqbidv 3129 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑚 → (∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
138 | 134, 137 | rspc 3276 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ → ∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
139 | 131, 138 | mpan9 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
140 | | nfcsb1v 3515 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
141 | 140 | nfel1 2765 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ |
142 | | csbeq1a 3508 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ⦋𝑚 / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
143 | 142 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔ ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
144 | 141, 143 | rspc 3276 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵 → (∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
145 | 139, 144 | syl5com 31 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → (𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵 → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
146 | 145 | impr 647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵)) → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
147 | 120, 88, 129, 146 | syl12anc 1316 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
148 | 147 | ralrimivva 2954 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ∀𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
149 | 148 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ∀𝑛 ∈ 𝐶 ∀𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
150 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑛 = (1st ‘𝑤) → ⦋𝑛 / 𝑘⦌𝐷 = ⦋(1st
‘𝑤) / 𝑘⦌𝐷) |
151 | | csbeq1 3502 |
. . . . . . . . . 10
⊢ (𝑛 = (1st ‘𝑤) → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = ⦋(1st
‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
152 | 151 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑛 = (1st ‘𝑤) → (⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔
⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
153 | 150, 152 | raleqbidv 3129 |
. . . . . . . 8
⊢ (𝑛 = (1st ‘𝑤) → (∀𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔ ∀𝑚 ∈ ⦋
(1st ‘𝑤) /
𝑘⦌𝐷⦋(1st
‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
154 | 153 | rspcv 3278 |
. . . . . . 7
⊢
((1st ‘𝑤) ∈ 𝐶 → (∀𝑛 ∈ 𝐶 ∀𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ → ∀𝑚 ∈ ⦋
(1st ‘𝑤) /
𝑘⦌𝐷⦋(1st
‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
155 | 119, 149,
154 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ∀𝑚 ∈ ⦋ (1st
‘𝑤) / 𝑘⦌𝐷⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
156 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑚 = (2nd ‘𝑤) → ⦋𝑚 / 𝑗⦌𝐸 = ⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
157 | 156 | csbeq2dv 3944 |
. . . . . . . 8
⊢ (𝑚 = (2nd ‘𝑤) →
⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
158 | 157 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑚 = (2nd ‘𝑤) →
(⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔
⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 ∈ ℂ)) |
159 | 158 | rspcv 3278 |
. . . . . 6
⊢
((2nd ‘𝑤) ∈ ⦋(1st
‘𝑤) / 𝑘⦌𝐷 → (∀𝑚 ∈ ⦋ (1st
‘𝑤) / 𝑘⦌𝐷⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ →
⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 ∈ ℂ)) |
160 | 115, 155,
159 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 ∈ ℂ) |
161 | 49, 55, 97, 102, 160 | fsumcnv 14346 |
. . . 4
⊢ (𝜑 → Σ𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = Σ𝑧 ∈ ◡ ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
162 | 41, 161 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → Σ𝑧 ∈ ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = Σ𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
163 | | fsumcom2.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) |
164 | 163 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ Fin) |
165 | 25 | nfel1 2765 |
. . . . . 6
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐵 ∈ Fin |
166 | 28 | eleq1d 2672 |
. . . . . 6
⊢ (𝑗 = 𝑚 → (𝐵 ∈ Fin ↔ ⦋𝑚 / 𝑗⦌𝐵 ∈ Fin)) |
167 | 165, 166 | rspc 3276 |
. . . . 5
⊢ (𝑚 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋𝑚 / 𝑗⦌𝐵 ∈ Fin)) |
168 | 164, 167 | mpan9 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑗⦌𝐵 ∈ Fin) |
169 | 55, 58, 168, 146 | fsum2d 14344 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = Σ𝑧 ∈ ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
170 | 49, 56, 92, 147 | fsum2d 14344 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝐶 Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = Σ𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
171 | 162, 169,
170 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = Σ𝑛 ∈ 𝐶 Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
172 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑚Σ𝑘 ∈ 𝐵 𝐸 |
173 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑗𝑛 |
174 | 173, 132 | nfcsb 3517 |
. . . 4
⊢
Ⅎ𝑗⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
175 | 25, 174 | nfsum 14269 |
. . 3
⊢
Ⅎ𝑗Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
176 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑛𝐸 |
177 | | nfcsb1v 3515 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐸 |
178 | | csbeq1a 3508 |
. . . . 5
⊢ (𝑘 = 𝑛 → 𝐸 = ⦋𝑛 / 𝑘⦌𝐸) |
179 | 176, 177,
178 | cbvsumi 14275 |
. . . 4
⊢
Σ𝑘 ∈
𝐵 𝐸 = Σ𝑛 ∈ 𝐵 ⦋𝑛 / 𝑘⦌𝐸 |
180 | 135 | csbeq2dv 3944 |
. . . . . 6
⊢ (𝑗 = 𝑚 → ⦋𝑛 / 𝑘⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
181 | 180 | adantr 480 |
. . . . 5
⊢ ((𝑗 = 𝑚 ∧ 𝑛 ∈ 𝐵) → ⦋𝑛 / 𝑘⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
182 | 28, 181 | sumeq12dv 14284 |
. . . 4
⊢ (𝑗 = 𝑚 → Σ𝑛 ∈ 𝐵 ⦋𝑛 / 𝑘⦌𝐸 = Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
183 | 179, 182 | syl5eq 2656 |
. . 3
⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
184 | 172, 175,
183 | cbvsumi 14275 |
. 2
⊢
Σ𝑗 ∈
𝐴 Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑚 ∈ 𝐴 Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
185 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑛Σ𝑗 ∈ 𝐷 𝐸 |
186 | 33, 140 | nfsum 14269 |
. . 3
⊢
Ⅎ𝑘Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
187 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑚𝐸 |
188 | 187, 132,
135 | cbvsumi 14275 |
. . . 4
⊢
Σ𝑗 ∈
𝐷 𝐸 = Σ𝑚 ∈ 𝐷 ⦋𝑚 / 𝑗⦌𝐸 |
189 | 142 | adantr 480 |
. . . . 5
⊢ ((𝑘 = 𝑛 ∧ 𝑚 ∈ 𝐷) → ⦋𝑚 / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
190 | 36, 189 | sumeq12dv 14284 |
. . . 4
⊢ (𝑘 = 𝑛 → Σ𝑚 ∈ 𝐷 ⦋𝑚 / 𝑗⦌𝐸 = Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
191 | 188, 190 | syl5eq 2656 |
. . 3
⊢ (𝑘 = 𝑛 → Σ𝑗 ∈ 𝐷 𝐸 = Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
192 | 185, 186,
191 | cbvsumi 14275 |
. 2
⊢
Σ𝑘 ∈
𝐶 Σ𝑗 ∈ 𝐷 𝐸 = Σ𝑛 ∈ 𝐶 Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
193 | 171, 184,
192 | 3eqtr4g 2669 |
1
⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑘 ∈ 𝐶 Σ𝑗 ∈ 𝐷 𝐸) |