| Step | Hyp | Ref
| Expression |
| 1 | | relxp 4772 |
. . . . . . . . 9
⊢ Rel
({𝑗} × 𝐵) |
| 2 | 1 | rgenw 2552 |
. . . . . . . 8
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐵) |
| 3 | | reliun 4784 |
. . . . . . . 8
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐵)) |
| 4 | 2, 3 | mpbir 146 |
. . . . . . 7
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
| 5 | | relcnv 5047 |
. . . . . . 7
⊢ Rel ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) |
| 6 | | ancom 266 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑗 ∧ 𝑦 = 𝑘) ↔ (𝑦 = 𝑘 ∧ 𝑥 = 𝑗)) |
| 7 | | vex 2766 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 8 | | vex 2766 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
| 9 | 7, 8 | opth 4270 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ (𝑥 = 𝑗 ∧ 𝑦 = 𝑘)) |
| 10 | 8, 7 | opth 4270 |
. . . . . . . . . . . 12
⊢
(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ↔ (𝑦 = 𝑘 ∧ 𝑥 = 𝑗)) |
| 11 | 6, 9, 10 | 3bitr4i 212 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉) |
| 12 | 11 | a1i 9 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉)) |
| 13 | | fsumcom2.4 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
| 14 | 12, 13 | anbi12d 473 |
. . . . . . . . 9
⊢ (𝜑 → ((〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) ↔ (〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)))) |
| 15 | 14 | 2exbidv 1882 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)))) |
| 16 | | eliunxp 4805 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
| 17 | 7, 8 | opelcnv 4848 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ 〈𝑦, 𝑥〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
| 18 | | eliunxp 4805 |
. . . . . . . . 9
⊢
(〈𝑦, 𝑥〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘∃𝑗(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
| 19 | | excom 1678 |
. . . . . . . . 9
⊢
(∃𝑘∃𝑗(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
| 20 | 17, 18, 19 | 3bitri 206 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
| 21 | 15, 16, 20 | 3bitr4g 223 |
. . . . . . 7
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷))) |
| 22 | 4, 5, 21 | eqrelrdv 4759 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
| 23 | | nfcv 2339 |
. . . . . . 7
⊢
Ⅎ𝑚({𝑗} × 𝐵) |
| 24 | | nfcv 2339 |
. . . . . . . 8
⊢
Ⅎ𝑗{𝑚} |
| 25 | | nfcsb1v 3117 |
. . . . . . . 8
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐵 |
| 26 | 24, 25 | nfxp 4690 |
. . . . . . 7
⊢
Ⅎ𝑗({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) |
| 27 | | sneq 3633 |
. . . . . . . 8
⊢ (𝑗 = 𝑚 → {𝑗} = {𝑚}) |
| 28 | | csbeq1a 3093 |
. . . . . . . 8
⊢ (𝑗 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑗⦌𝐵) |
| 29 | 27, 28 | xpeq12d 4688 |
. . . . . . 7
⊢ (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)) |
| 30 | 23, 26, 29 | cbviun 3953 |
. . . . . 6
⊢ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) |
| 31 | | nfcv 2339 |
. . . . . . . 8
⊢
Ⅎ𝑛({𝑘} × 𝐷) |
| 32 | | nfcv 2339 |
. . . . . . . . 9
⊢
Ⅎ𝑘{𝑛} |
| 33 | | nfcsb1v 3117 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐷 |
| 34 | 32, 33 | nfxp 4690 |
. . . . . . . 8
⊢
Ⅎ𝑘({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
| 35 | | sneq 3633 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → {𝑘} = {𝑛}) |
| 36 | | csbeq1a 3093 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → 𝐷 = ⦋𝑛 / 𝑘⦌𝐷) |
| 37 | 35, 36 | xpeq12d 4688 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ({𝑘} × 𝐷) = ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 38 | 31, 34, 37 | cbviun 3953 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) = ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
| 39 | 38 | cnveqi 4841 |
. . . . . 6
⊢ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) = ◡∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
| 40 | 22, 30, 39 | 3eqtr3g 2252 |
. . . . 5
⊢ (𝜑 → ∪ 𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵) = ◡∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 41 | 40 | sumeq1d 11531 |
. . . 4
⊢ (𝜑 → Σ𝑧 ∈ ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = Σ𝑧 ∈ ◡ ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
| 42 | | vex 2766 |
. . . . . . . 8
⊢ 𝑛 ∈ V |
| 43 | | vex 2766 |
. . . . . . . 8
⊢ 𝑚 ∈ V |
| 44 | 42, 43 | op1std 6206 |
. . . . . . 7
⊢ (𝑤 = 〈𝑛, 𝑚〉 → (1st ‘𝑤) = 𝑛) |
| 45 | 44 | csbeq1d 3091 |
. . . . . 6
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
| 46 | 42, 43 | op2ndd 6207 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑛, 𝑚〉 → (2nd ‘𝑤) = 𝑚) |
| 47 | 46 | csbeq1d 3091 |
. . . . . . 7
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑚 / 𝑗⦌𝐸) |
| 48 | 47 | csbeq2dv 3110 |
. . . . . 6
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋𝑛 / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 49 | 45, 48 | eqtrd 2229 |
. . . . 5
⊢ (𝑤 = 〈𝑛, 𝑚〉 → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 50 | 43, 42 | op2ndd 6207 |
. . . . . . 7
⊢ (𝑧 = 〈𝑚, 𝑛〉 → (2nd ‘𝑧) = 𝑛) |
| 51 | 50 | csbeq1d 3091 |
. . . . . 6
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋(2nd
‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
| 52 | 43, 42 | op1std 6206 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑚, 𝑛〉 → (1st ‘𝑧) = 𝑚) |
| 53 | 52 | csbeq1d 3091 |
. . . . . . 7
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑚 / 𝑗⦌𝐸) |
| 54 | 53 | csbeq2dv 3110 |
. . . . . 6
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋𝑛 / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 55 | 51, 54 | eqtrd 2229 |
. . . . 5
⊢ (𝑧 = 〈𝑚, 𝑛〉 → ⦋(2nd
‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 56 | | fsumcom2.2 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Fin) |
| 57 | | snfig 6873 |
. . . . . . . . 9
⊢ (𝑛 ∈ V → {𝑛} ∈ Fin) |
| 58 | 57 | elv 2767 |
. . . . . . . 8
⊢ {𝑛} ∈ Fin |
| 59 | | fisumcom2.fi |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ Fin) |
| 60 | 59 | ralrimiva 2570 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐶 𝐷 ∈ Fin) |
| 61 | 33 | nfel1 2350 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐷 ∈ Fin |
| 62 | 36 | eleq1d 2265 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝐷 ∈ Fin ↔ ⦋𝑛 / 𝑘⦌𝐷 ∈ Fin)) |
| 63 | 61, 62 | rspc 2862 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐶 → (∀𝑘 ∈ 𝐶 𝐷 ∈ Fin → ⦋𝑛 / 𝑘⦌𝐷 ∈ Fin)) |
| 64 | 60, 63 | mpan9 281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋𝑛 / 𝑘⦌𝐷 ∈ Fin) |
| 65 | | xpfi 6993 |
. . . . . . . 8
⊢ (({𝑛} ∈ Fin ∧
⦋𝑛 / 𝑘⦌𝐷 ∈ Fin) → ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
| 66 | 58, 64, 65 | sylancr 414 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
| 67 | 66 | ralrimiva 2570 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
| 68 | | disjsnxp 6295 |
. . . . . . 7
⊢
Disj 𝑛 ∈
𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
| 69 | 68 | a1i 9 |
. . . . . 6
⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 70 | | iunfidisj 7012 |
. . . . . 6
⊢ ((𝐶 ∈ Fin ∧ ∀𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin ∧ Disj 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
| 71 | 56, 67, 69, 70 | syl3anc 1249 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ∈ Fin) |
| 72 | | reliun 4784 |
. . . . . . 7
⊢ (Rel
∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ↔ ∀𝑛 ∈ 𝐶 Rel ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 73 | | relxp 4772 |
. . . . . . . 8
⊢ Rel
({𝑛} ×
⦋𝑛 / 𝑘⦌𝐷) |
| 74 | 73 | a1i 9 |
. . . . . . 7
⊢ (𝑛 ∈ 𝐶 → Rel ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 75 | 72, 74 | mprgbir 2555 |
. . . . . 6
⊢ Rel
∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) |
| 76 | 75 | a1i 9 |
. . . . 5
⊢ (𝜑 → Rel ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 77 | | csbeq1 3087 |
. . . . . . . 8
⊢ (𝑚 = (2nd ‘𝑤) → ⦋𝑚 / 𝑗⦌𝐸 = ⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
| 78 | 77 | csbeq2dv 3110 |
. . . . . . 7
⊢ (𝑚 = (2nd ‘𝑤) →
⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
| 79 | 78 | eleq1d 2265 |
. . . . . 6
⊢ (𝑚 = (2nd ‘𝑤) →
(⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔
⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 ∈ ℂ)) |
| 80 | | csbeq1 3087 |
. . . . . . . 8
⊢ (𝑛 = (1st ‘𝑤) → ⦋𝑛 / 𝑘⦌𝐷 = ⦋(1st
‘𝑤) / 𝑘⦌𝐷) |
| 81 | | csbeq1 3087 |
. . . . . . . . 9
⊢ (𝑛 = (1st ‘𝑤) → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = ⦋(1st
‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 82 | 81 | eleq1d 2265 |
. . . . . . . 8
⊢ (𝑛 = (1st ‘𝑤) → (⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔
⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 83 | 80, 82 | raleqbidv 2709 |
. . . . . . 7
⊢ (𝑛 = (1st ‘𝑤) → (∀𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔ ∀𝑚 ∈ ⦋
(1st ‘𝑤) /
𝑘⦌𝐷⦋(1st
‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 84 | | simpl 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 𝜑) |
| 85 | 43, 42 | opelcnv 4848 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑚, 𝑛〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ 〈𝑛, 𝑚〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
| 86 | 33, 36 | opeliunxp2f 6296 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑛, 𝑚〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) |
| 87 | 85, 86 | sylbbr 136 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷) → 〈𝑚, 𝑛〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
| 88 | 87 | adantl 277 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 〈𝑚, 𝑛〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
| 89 | 22 | adantr 276 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
| 90 | 88, 89 | eleqtrrd 2276 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 〈𝑚, 𝑛〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 91 | | eliun 3920 |
. . . . . . . . . . . 12
⊢
(〈𝑚, 𝑛〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) |
| 92 | 90, 91 | sylib 122 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → ∃𝑗 ∈ 𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) |
| 93 | | simpr 110 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) |
| 94 | | opelxp 4693 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) ↔ (𝑚 ∈ {𝑗} ∧ 𝑛 ∈ 𝐵)) |
| 95 | 93, 94 | sylib 122 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → (𝑚 ∈ {𝑗} ∧ 𝑛 ∈ 𝐵)) |
| 96 | 95 | simpld 112 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑚 ∈ {𝑗}) |
| 97 | | elsni 3640 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ {𝑗} → 𝑚 = 𝑗) |
| 98 | 96, 97 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑚 = 𝑗) |
| 99 | | simpl 109 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑗 ∈ 𝐴) |
| 100 | 98, 99 | eqeltrd 2273 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵)) → 𝑚 ∈ 𝐴) |
| 101 | 100 | rexlimiva 2609 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑚 ∈ 𝐴) |
| 102 | 92, 101 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 𝑚 ∈ 𝐴) |
| 103 | 25 | nfcri 2333 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵 |
| 104 | 97 | equcomd 1721 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ {𝑗} → 𝑗 = 𝑚) |
| 105 | 104, 28 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ {𝑗} → 𝐵 = ⦋𝑚 / 𝑗⦌𝐵) |
| 106 | 105 | eleq2d 2266 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑗} → (𝑛 ∈ 𝐵 ↔ 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵)) |
| 107 | 106 | biimpa 296 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ {𝑗} ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
| 108 | 94, 107 | sylbi 121 |
. . . . . . . . . . . . 13
⊢
(〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
| 109 | 108 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ 𝐴 → (〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵)) |
| 110 | 103, 109 | rexlimi 2607 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
𝐴 〈𝑚, 𝑛〉 ∈ ({𝑗} × 𝐵) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
| 111 | 92, 110 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵) |
| 112 | | fsumcom2.5 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐸 ∈ ℂ) |
| 113 | 112 | ralrimivva 2579 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ) |
| 114 | | nfcsb1v 3117 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐸 |
| 115 | 114 | nfel1 2350 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ |
| 116 | 25, 115 | nfralxy 2535 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ |
| 117 | | csbeq1a 3093 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑚 → 𝐸 = ⦋𝑚 / 𝑗⦌𝐸) |
| 118 | 117 | eleq1d 2265 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑚 → (𝐸 ∈ ℂ ↔ ⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 119 | 28, 118 | raleqbidv 2709 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑚 → (∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 120 | 116, 119 | rspc 2862 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ → ∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 121 | 113, 120 | mpan9 281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
| 122 | | nfcsb1v 3117 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
| 123 | 122 | nfel1 2350 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ |
| 124 | | csbeq1a 3093 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ⦋𝑚 / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 125 | 124 | eleq1d 2265 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ ↔ ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 126 | 123, 125 | rspc 2862 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵 → (∀𝑘 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 127 | 121, 126 | syl5com 29 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → (𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵 → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ)) |
| 128 | 127 | impr 379 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ 𝐴 ∧ 𝑛 ∈ ⦋𝑚 / 𝑗⦌𝐵)) → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
| 129 | 84, 102, 111, 128 | syl12anc 1247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ 𝐶 ∧ 𝑚 ∈ ⦋𝑛 / 𝑘⦌𝐷)) → ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
| 130 | 129 | ralrimivva 2579 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ∀𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
| 131 | 130 | adantr 276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ∀𝑛 ∈ 𝐶 ∀𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
| 132 | | simpr 110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 133 | | eliun 3920 |
. . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) ↔ ∃𝑛 ∈ 𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 134 | 132, 133 | sylib 122 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ∃𝑛 ∈ 𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) |
| 135 | | xp1st 6223 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (1st ‘𝑤) ∈ {𝑛}) |
| 136 | 135 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ {𝑛}) |
| 137 | | elsni 3640 |
. . . . . . . . . . 11
⊢
((1st ‘𝑤) ∈ {𝑛} → (1st ‘𝑤) = 𝑛) |
| 138 | 136, 137 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) = 𝑛) |
| 139 | | simpl 109 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → 𝑛 ∈ 𝐶) |
| 140 | 138, 139 | eqeltrd 2273 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ 𝐶) |
| 141 | 140 | rexlimiva 2609 |
. . . . . . . 8
⊢
(∃𝑛 ∈
𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (1st ‘𝑤) ∈ 𝐶) |
| 142 | 134, 141 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ 𝐶) |
| 143 | 83, 131, 142 | rspcdva 2873 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ∀𝑚 ∈ ⦋ (1st
‘𝑤) / 𝑘⦌𝐷⦋(1st ‘𝑤) / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 ∈ ℂ) |
| 144 | | xp2nd 6224 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (2nd ‘𝑤) ∈ ⦋𝑛 / 𝑘⦌𝐷) |
| 145 | 144 | adantl 277 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈ ⦋𝑛 / 𝑘⦌𝐷) |
| 146 | 138 | csbeq1d 3091 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ⦋(1st
‘𝑤) / 𝑘⦌𝐷 = ⦋𝑛 / 𝑘⦌𝐷) |
| 147 | 145, 146 | eleqtrrd 2276 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
| 148 | 147 | rexlimiva 2609 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝐶 𝑤 ∈ ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
| 149 | 134, 148 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
| 150 | 79, 143, 149 | rspcdva 2873 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)) → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 ∈ ℂ) |
| 151 | 49, 55, 71, 76, 150 | fsumcnv 11602 |
. . . 4
⊢ (𝜑 → Σ𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = Σ𝑧 ∈ ◡ ∪ 𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
| 152 | 41, 151 | eqtr4d 2232 |
. . 3
⊢ (𝜑 → Σ𝑧 ∈ ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = Σ𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
| 153 | | fsumcom2.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 154 | | fsumcom2.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) |
| 155 | 154 | ralrimiva 2570 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ Fin) |
| 156 | 25 | nfel1 2350 |
. . . . . 6
⊢
Ⅎ𝑗⦋𝑚 / 𝑗⦌𝐵 ∈ Fin |
| 157 | 28 | eleq1d 2265 |
. . . . . 6
⊢ (𝑗 = 𝑚 → (𝐵 ∈ Fin ↔ ⦋𝑚 / 𝑗⦌𝐵 ∈ Fin)) |
| 158 | 156, 157 | rspc 2862 |
. . . . 5
⊢ (𝑚 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋𝑚 / 𝑗⦌𝐵 ∈ Fin)) |
| 159 | 155, 158 | mpan9 281 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑗⦌𝐵 ∈ Fin) |
| 160 | 55, 153, 159, 128 | fsum2d 11600 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = Σ𝑧 ∈ ∪
𝑚 ∈ 𝐴 ({𝑚} × ⦋𝑚 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
| 161 | 49, 56, 64, 129 | fsum2d 11600 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ 𝐶 Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = Σ𝑤 ∈ ∪
𝑛 ∈ 𝐶 ({𝑛} × ⦋𝑛 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
| 162 | 152, 160,
161 | 3eqtr4d 2239 |
. 2
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 = Σ𝑛 ∈ 𝐶 Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 163 | | nfcv 2339 |
. . 3
⊢
Ⅎ𝑚Σ𝑘 ∈ 𝐵 𝐸 |
| 164 | | nfcv 2339 |
. . . . 5
⊢
Ⅎ𝑗𝑛 |
| 165 | 164, 114 | nfcsb 3122 |
. . . 4
⊢
Ⅎ𝑗⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
| 166 | 25, 165 | nfsum 11522 |
. . 3
⊢
Ⅎ𝑗Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
| 167 | | nfcv 2339 |
. . . . 5
⊢
Ⅎ𝑛𝐸 |
| 168 | | nfcsb1v 3117 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐸 |
| 169 | | csbeq1a 3093 |
. . . . 5
⊢ (𝑘 = 𝑛 → 𝐸 = ⦋𝑛 / 𝑘⦌𝐸) |
| 170 | 167, 168,
169 | cbvsumi 11527 |
. . . 4
⊢
Σ𝑘 ∈
𝐵 𝐸 = Σ𝑛 ∈ 𝐵 ⦋𝑛 / 𝑘⦌𝐸 |
| 171 | 117 | csbeq2dv 3110 |
. . . . . 6
⊢ (𝑗 = 𝑚 → ⦋𝑛 / 𝑘⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 172 | 171 | adantr 276 |
. . . . 5
⊢ ((𝑗 = 𝑚 ∧ 𝑛 ∈ 𝐵) → ⦋𝑛 / 𝑘⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 173 | 28, 172 | sumeq12dv 11537 |
. . . 4
⊢ (𝑗 = 𝑚 → Σ𝑛 ∈ 𝐵 ⦋𝑛 / 𝑘⦌𝐸 = Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 174 | 170, 173 | eqtrid 2241 |
. . 3
⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 175 | 163, 166,
174 | cbvsumi 11527 |
. 2
⊢
Σ𝑗 ∈
𝐴 Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑚 ∈ 𝐴 Σ𝑛 ∈ ⦋ 𝑚 / 𝑗⦌𝐵⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
| 176 | | nfcv 2339 |
. . 3
⊢
Ⅎ𝑛Σ𝑗 ∈ 𝐷 𝐸 |
| 177 | 33, 122 | nfsum 11522 |
. . 3
⊢
Ⅎ𝑘Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
| 178 | | nfcv 2339 |
. . . . 5
⊢
Ⅎ𝑚𝐸 |
| 179 | 178, 114,
117 | cbvsumi 11527 |
. . . 4
⊢
Σ𝑗 ∈
𝐷 𝐸 = Σ𝑚 ∈ 𝐷 ⦋𝑚 / 𝑗⦌𝐸 |
| 180 | 124 | adantr 276 |
. . . . 5
⊢ ((𝑘 = 𝑛 ∧ 𝑚 ∈ 𝐷) → ⦋𝑚 / 𝑗⦌𝐸 = ⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 181 | 36, 180 | sumeq12dv 11537 |
. . . 4
⊢ (𝑘 = 𝑛 → Σ𝑚 ∈ 𝐷 ⦋𝑚 / 𝑗⦌𝐸 = Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 182 | 179, 181 | eqtrid 2241 |
. . 3
⊢ (𝑘 = 𝑛 → Σ𝑗 ∈ 𝐷 𝐸 = Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸) |
| 183 | 176, 177,
182 | cbvsumi 11527 |
. 2
⊢
Σ𝑘 ∈
𝐶 Σ𝑗 ∈ 𝐷 𝐸 = Σ𝑛 ∈ 𝐶 Σ𝑚 ∈ ⦋ 𝑛 / 𝑘⦌𝐷⦋𝑛 / 𝑘⦌⦋𝑚 / 𝑗⦌𝐸 |
| 184 | 162, 175,
183 | 3eqtr4g 2254 |
1
⊢ (𝜑 → Σ𝑗 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐸 = Σ𝑘 ∈ 𝐶 Σ𝑗 ∈ 𝐷 𝐸) |