Step | Hyp | Ref
| Expression |
1 | | relxp 4697 |
. . . . . . . . 9
⊢ Rel
({𝑗} × 𝐵) |
2 | 1 | rgenw 2512 |
. . . . . . . 8
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐵) |
3 | | reliun 4709 |
. . . . . . . 8
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐵)) |
4 | 2, 3 | mpbir 145 |
. . . . . . 7
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
5 | | relcnv 4966 |
. . . . . . 7
⊢ Rel ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) |
6 | | ancom 264 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑗 ∧ 𝑦 = 𝑘) ↔ (𝑦 = 𝑘 ∧ 𝑥 = 𝑗)) |
7 | | vex 2715 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
8 | | vex 2715 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
9 | 7, 8 | opth 4199 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ (𝑥 = 𝑗 ∧ 𝑦 = 𝑘)) |
10 | 8, 7 | opth 4199 |
. . . . . . . . . . . 12
⊢
(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ↔ (𝑦 = 𝑘 ∧ 𝑥 = 𝑗)) |
11 | 6, 9, 10 | 3bitr4i 211 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉) |
12 | 11 | a1i 9 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ↔ 〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉)) |
13 | | fprodcom2.4 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
14 | 12, 13 | anbi12d 465 |
. . . . . . . . 9
⊢ (𝜑 → ((〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) ↔ (〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)))) |
15 | 14 | 2exbidv 1848 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)))) |
16 | | eliunxp 4727 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
17 | 7, 8 | opelcnv 4770 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ 〈𝑦, 𝑥〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
18 | | eliunxp 4727 |
. . . . . . . . 9
⊢
(〈𝑦, 𝑥〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ ∃𝑘∃𝑗(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
19 | | excom 1644 |
. . . . . . . . 9
⊢
(∃𝑘∃𝑗(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷)) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
20 | 17, 18, 19 | 3bitri 205 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ ∃𝑗∃𝑘(〈𝑦, 𝑥〉 = 〈𝑘, 𝑗〉 ∧ (𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷))) |
21 | 15, 16, 20 | 3bitr4g 222 |
. . . . . . 7
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷))) |
22 | 4, 5, 21 | eqrelrdv 4684 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
23 | | nfcv 2299 |
. . . . . . 7
⊢
Ⅎ𝑥({𝑗} × 𝐵) |
24 | | nfcv 2299 |
. . . . . . . 8
⊢
Ⅎ𝑗{𝑥} |
25 | | nfcsb1v 3064 |
. . . . . . . 8
⊢
Ⅎ𝑗⦋𝑥 / 𝑗⦌𝐵 |
26 | 24, 25 | nfxp 4615 |
. . . . . . 7
⊢
Ⅎ𝑗({𝑥} × ⦋𝑥 / 𝑗⦌𝐵) |
27 | | sneq 3572 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥}) |
28 | | csbeq1a 3040 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → 𝐵 = ⦋𝑥 / 𝑗⦌𝐵) |
29 | 27, 28 | xpeq12d 4613 |
. . . . . . 7
⊢ (𝑗 = 𝑥 → ({𝑗} × 𝐵) = ({𝑥} × ⦋𝑥 / 𝑗⦌𝐵)) |
30 | 23, 26, 29 | cbviun 3888 |
. . . . . 6
⊢ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ∪
𝑥 ∈ 𝐴 ({𝑥} × ⦋𝑥 / 𝑗⦌𝐵) |
31 | | nfcv 2299 |
. . . . . . . 8
⊢
Ⅎ𝑦({𝑘} × 𝐷) |
32 | | nfcv 2299 |
. . . . . . . . 9
⊢
Ⅎ𝑘{𝑦} |
33 | | nfcsb1v 3064 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐷 |
34 | 32, 33 | nfxp 4615 |
. . . . . . . 8
⊢
Ⅎ𝑘({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) |
35 | | sneq 3572 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → {𝑘} = {𝑦}) |
36 | | csbeq1a 3040 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → 𝐷 = ⦋𝑦 / 𝑘⦌𝐷) |
37 | 35, 36 | xpeq12d 4613 |
. . . . . . . 8
⊢ (𝑘 = 𝑦 → ({𝑘} × 𝐷) = ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
38 | 31, 34, 37 | cbviun 3888 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) = ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) |
39 | 38 | cnveqi 4763 |
. . . . . 6
⊢ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) = ◡∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) |
40 | 22, 30, 39 | 3eqtr3g 2213 |
. . . . 5
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × ⦋𝑥 / 𝑗⦌𝐵) = ◡∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
41 | 40 | prodeq1d 11472 |
. . . 4
⊢ (𝜑 → ∏𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × ⦋𝑥 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ∏𝑧 ∈ ◡ ∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
42 | 8, 7 | op1std 6098 |
. . . . . . 7
⊢ (𝑤 = 〈𝑦, 𝑥〉 → (1st ‘𝑤) = 𝑦) |
43 | 42 | csbeq1d 3038 |
. . . . . 6
⊢ (𝑤 = 〈𝑦, 𝑥〉 → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
44 | 8, 7 | op2ndd 6099 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑦, 𝑥〉 → (2nd ‘𝑤) = 𝑥) |
45 | 44 | csbeq1d 3038 |
. . . . . . 7
⊢ (𝑤 = 〈𝑦, 𝑥〉 → ⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑥 / 𝑗⦌𝐸) |
46 | 45 | csbeq2dv 3057 |
. . . . . 6
⊢ (𝑤 = 〈𝑦, 𝑥〉 → ⦋𝑦 / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
47 | 43, 46 | eqtrd 2190 |
. . . . 5
⊢ (𝑤 = 〈𝑦, 𝑥〉 → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
48 | 7, 8 | op2ndd 6099 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
49 | 48 | csbeq1d 3038 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ⦋(2nd
‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
50 | 7, 8 | op1std 6098 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
51 | 50 | csbeq1d 3038 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑥 / 𝑗⦌𝐸) |
52 | 51 | csbeq2dv 3057 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ⦋𝑦 / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
53 | 49, 52 | eqtrd 2190 |
. . . . 5
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ⦋(2nd
‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
54 | | fprodcom2.2 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Fin) |
55 | | snfig 6761 |
. . . . . . . . 9
⊢ (𝑦 ∈ V → {𝑦} ∈ Fin) |
56 | 55 | elv 2716 |
. . . . . . . 8
⊢ {𝑦} ∈ Fin |
57 | | fprodcom2fi.d |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ Fin) |
58 | 57 | ralrimiva 2530 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐶 𝐷 ∈ Fin) |
59 | 33 | nfel1 2310 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐷 ∈ Fin |
60 | 36 | eleq1d 2226 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → (𝐷 ∈ Fin ↔ ⦋𝑦 / 𝑘⦌𝐷 ∈ Fin)) |
61 | 59, 60 | rspc 2810 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐶 → (∀𝑘 ∈ 𝐶 𝐷 ∈ Fin → ⦋𝑦 / 𝑘⦌𝐷 ∈ Fin)) |
62 | 58, 61 | mpan9 279 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ⦋𝑦 / 𝑘⦌𝐷 ∈ Fin) |
63 | | xpfi 6876 |
. . . . . . . 8
⊢ (({𝑦} ∈ Fin ∧
⦋𝑦 / 𝑘⦌𝐷 ∈ Fin) → ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ∈ Fin) |
64 | 56, 62, 63 | sylancr 411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ∈ Fin) |
65 | 64 | ralrimiva 2530 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ∈ Fin) |
66 | | disjsnxp 6186 |
. . . . . . 7
⊢
Disj 𝑦 ∈
𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) |
67 | 66 | a1i 9 |
. . . . . 6
⊢ (𝜑 → Disj 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
68 | | iunfidisj 6892 |
. . . . . 6
⊢ ((𝐶 ∈ Fin ∧ ∀𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ∈ Fin ∧ Disj 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → ∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ∈ Fin) |
69 | 54, 65, 67, 68 | syl3anc 1220 |
. . . . 5
⊢ (𝜑 → ∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ∈ Fin) |
70 | | reliun 4709 |
. . . . . . 7
⊢ (Rel
∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ↔ ∀𝑦 ∈ 𝐶 Rel ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
71 | | relxp 4697 |
. . . . . . . 8
⊢ Rel
({𝑦} ×
⦋𝑦 / 𝑘⦌𝐷) |
72 | 71 | a1i 9 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐶 → Rel ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
73 | 70, 72 | mprgbir 2515 |
. . . . . 6
⊢ Rel
∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) |
74 | 73 | a1i 9 |
. . . . 5
⊢ (𝜑 → Rel ∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
75 | | csbeq1 3034 |
. . . . . . . 8
⊢ (𝑥 = (2nd ‘𝑤) → ⦋𝑥 / 𝑗⦌𝐸 = ⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
76 | 75 | csbeq2dv 3057 |
. . . . . . 7
⊢ (𝑥 = (2nd ‘𝑤) →
⦋(1st ‘𝑤) / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 = ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
77 | 76 | eleq1d 2226 |
. . . . . 6
⊢ (𝑥 = (2nd ‘𝑤) →
(⦋(1st ‘𝑤) / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ ↔
⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 ∈ ℂ)) |
78 | | csbeq1 3034 |
. . . . . . . 8
⊢ (𝑦 = (1st ‘𝑤) → ⦋𝑦 / 𝑘⦌𝐷 = ⦋(1st
‘𝑤) / 𝑘⦌𝐷) |
79 | | csbeq1 3034 |
. . . . . . . . 9
⊢ (𝑦 = (1st ‘𝑤) → ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 = ⦋(1st
‘𝑤) / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
80 | 79 | eleq1d 2226 |
. . . . . . . 8
⊢ (𝑦 = (1st ‘𝑤) → (⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ ↔
⦋(1st ‘𝑤) / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
81 | 78, 80 | raleqbidv 2664 |
. . . . . . 7
⊢ (𝑦 = (1st ‘𝑤) → (∀𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ ↔ ∀𝑥 ∈ ⦋
(1st ‘𝑤) /
𝑘⦌𝐷⦋(1st
‘𝑤) / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
82 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → 𝜑) |
83 | 33, 36 | opeliunxp2f 6187 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑦, 𝑥〉 ∈ ∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) |
84 | 17, 83 | sylbbr 135 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷) → 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
85 | 84 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
86 | 22 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ◡∪ 𝑘 ∈ 𝐶 ({𝑘} × 𝐷)) |
87 | 85, 86 | eleqtrrd 2237 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → 〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
88 | | eliun 3855 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) |
89 | 87, 88 | sylib 121 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → ∃𝑗 ∈ 𝐴 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) |
90 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) → 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) |
91 | | opelxp 4618 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵) ↔ (𝑥 ∈ {𝑗} ∧ 𝑦 ∈ 𝐵)) |
92 | 90, 91 | sylib 121 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) → (𝑥 ∈ {𝑗} ∧ 𝑦 ∈ 𝐵)) |
93 | 92 | simpld 111 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) → 𝑥 ∈ {𝑗}) |
94 | | elsni 3579 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑗} → 𝑥 = 𝑗) |
95 | 93, 94 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) → 𝑥 = 𝑗) |
96 | | simpl 108 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) → 𝑗 ∈ 𝐴) |
97 | 95, 96 | eqeltrd 2234 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵)) → 𝑥 ∈ 𝐴) |
98 | 97 | rexlimiva 2569 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
𝐴 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵) → 𝑥 ∈ 𝐴) |
99 | 89, 98 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → 𝑥 ∈ 𝐴) |
100 | 25 | nfcri 2293 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵 |
101 | 94 | equcomd 1687 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑗} → 𝑗 = 𝑥) |
102 | 101, 28 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑗} → 𝐵 = ⦋𝑥 / 𝑗⦌𝐵) |
103 | 102 | eleq2d 2227 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝑗} → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵)) |
104 | 103 | biimpa 294 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ {𝑗} ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵) |
105 | 91, 104 | sylbi 120 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵) → 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵) |
106 | 105 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵) → 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵)) |
107 | 100, 106 | rexlimi 2567 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
𝐴 〈𝑥, 𝑦〉 ∈ ({𝑗} × 𝐵) → 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵) |
108 | 89, 107 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵) |
109 | | fprodcom2.5 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐸 ∈ ℂ) |
110 | 109 | ralrimivva 2539 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ) |
111 | | nfcsb1v 3064 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗⦋𝑥 / 𝑗⦌𝐸 |
112 | 111 | nfel1 2310 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ |
113 | 25, 112 | nfralw 2494 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗∀𝑘 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ |
114 | | csbeq1a 3040 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑥 → 𝐸 = ⦋𝑥 / 𝑗⦌𝐸) |
115 | 114 | eleq1d 2226 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑥 → (𝐸 ∈ ℂ ↔ ⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
116 | 28, 115 | raleqbidv 2664 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑥 → (∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ ↔ ∀𝑘 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
117 | 113, 116 | rspc 2810 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐵 𝐸 ∈ ℂ → ∀𝑘 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
118 | 110, 117 | mpan9 279 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ) |
119 | | nfcsb1v 3064 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 |
120 | 119 | nfel1 2310 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ |
121 | | csbeq1a 3040 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑦 → ⦋𝑥 / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
122 | 121 | eleq1d 2226 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ ↔ ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
123 | 120, 122 | rspc 2810 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵 → (∀𝑘 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ → ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
124 | 118, 123 | syl5com 29 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵 → ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ)) |
125 | 124 | impr 377 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ⦋𝑥 / 𝑗⦌𝐵)) → ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ) |
126 | 82, 99, 108, 125 | syl12anc 1218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋𝑦 / 𝑘⦌𝐷)) → ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ) |
127 | 126 | ralrimivva 2539 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ 𝐶 ∀𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ) |
128 | 127 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → ∀𝑦 ∈ 𝐶 ∀𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ) |
129 | | simpr 109 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
130 | | eliun 3855 |
. . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) ↔ ∃𝑦 ∈ 𝐶 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
131 | 129, 130 | sylib 121 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → ∃𝑦 ∈ 𝐶 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) |
132 | | xp1st 6115 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) → (1st ‘𝑤) ∈ {𝑦}) |
133 | 132 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ {𝑦}) |
134 | | elsni 3579 |
. . . . . . . . . . 11
⊢
((1st ‘𝑤) ∈ {𝑦} → (1st ‘𝑤) = 𝑦) |
135 | 133, 134 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → (1st ‘𝑤) = 𝑦) |
136 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → 𝑦 ∈ 𝐶) |
137 | 135, 136 | eqeltrd 2234 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ 𝐶) |
138 | 137 | rexlimiva 2569 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐶 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) → (1st ‘𝑤) ∈ 𝐶) |
139 | 131, 138 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → (1st ‘𝑤) ∈ 𝐶) |
140 | 81, 128, 139 | rspcdva 2821 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → ∀𝑥 ∈ ⦋ (1st
‘𝑤) / 𝑘⦌𝐷⦋(1st ‘𝑤) / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 ∈ ℂ) |
141 | | xp2nd 6116 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) → (2nd ‘𝑤) ∈ ⦋𝑦 / 𝑘⦌𝐷) |
142 | 141 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈ ⦋𝑦 / 𝑘⦌𝐷) |
143 | 135 | csbeq1d 3038 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → ⦋(1st
‘𝑤) / 𝑘⦌𝐷 = ⦋𝑦 / 𝑘⦌𝐷) |
144 | 142, 143 | eleqtrrd 2237 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
145 | 144 | rexlimiva 2569 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐶 𝑤 ∈ ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
146 | 131, 145 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → (2nd ‘𝑤) ∈
⦋(1st ‘𝑤) / 𝑘⦌𝐷) |
147 | 77, 140, 146 | rspcdva 2821 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)) → ⦋(1st
‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 ∈ ℂ) |
148 | 47, 53, 69, 74, 147 | fprodcnv 11533 |
. . . 4
⊢ (𝜑 → ∏𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸 = ∏𝑧 ∈ ◡ ∪ 𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
149 | 41, 148 | eqtr4d 2193 |
. . 3
⊢ (𝜑 → ∏𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × ⦋𝑥 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸 = ∏𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
150 | | fprodcom2.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
151 | | fprodcom2.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) |
152 | 151 | ralrimiva 2530 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ Fin) |
153 | 25 | nfel1 2310 |
. . . . . 6
⊢
Ⅎ𝑗⦋𝑥 / 𝑗⦌𝐵 ∈ Fin |
154 | 28 | eleq1d 2226 |
. . . . . 6
⊢ (𝑗 = 𝑥 → (𝐵 ∈ Fin ↔ ⦋𝑥 / 𝑗⦌𝐵 ∈ Fin)) |
155 | 153, 154 | rspc 2810 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋𝑥 / 𝑗⦌𝐵 ∈ Fin)) |
156 | 152, 155 | mpan9 279 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ⦋𝑥 / 𝑗⦌𝐵 ∈ Fin) |
157 | 53, 150, 156, 125 | fprod2d 11531 |
. . 3
⊢ (𝜑 → ∏𝑥 ∈ 𝐴 ∏𝑦 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 = ∏𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × ⦋𝑥 / 𝑗⦌𝐵)⦋(2nd ‘𝑧) / 𝑘⦌⦋(1st
‘𝑧) / 𝑗⦌𝐸) |
158 | 47, 54, 62, 126 | fprod2d 11531 |
. . 3
⊢ (𝜑 → ∏𝑦 ∈ 𝐶 ∏𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 = ∏𝑤 ∈ ∪
𝑦 ∈ 𝐶 ({𝑦} × ⦋𝑦 / 𝑘⦌𝐷)⦋(1st ‘𝑤) / 𝑘⦌⦋(2nd
‘𝑤) / 𝑗⦌𝐸) |
159 | 149, 157,
158 | 3eqtr4d 2200 |
. 2
⊢ (𝜑 → ∏𝑥 ∈ 𝐴 ∏𝑦 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 = ∏𝑦 ∈ 𝐶 ∏𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
160 | | nfcv 2299 |
. . 3
⊢
Ⅎ𝑥∏𝑘 ∈ 𝐵 𝐸 |
161 | | nfcv 2299 |
. . . . 5
⊢
Ⅎ𝑗𝑦 |
162 | 161, 111 | nfcsbw 3067 |
. . . 4
⊢
Ⅎ𝑗⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 |
163 | 25, 162 | nfcprod 11463 |
. . 3
⊢
Ⅎ𝑗∏𝑦 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 |
164 | | nfcv 2299 |
. . . . 5
⊢
Ⅎ𝑦𝐸 |
165 | | nfcsb1v 3064 |
. . . . 5
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐸 |
166 | | csbeq1a 3040 |
. . . . 5
⊢ (𝑘 = 𝑦 → 𝐸 = ⦋𝑦 / 𝑘⦌𝐸) |
167 | 164, 165,
166 | cbvprodi 11468 |
. . . 4
⊢
∏𝑘 ∈
𝐵 𝐸 = ∏𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐸 |
168 | 114 | csbeq2dv 3057 |
. . . . . 6
⊢ (𝑗 = 𝑥 → ⦋𝑦 / 𝑘⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
169 | 168 | adantr 274 |
. . . . 5
⊢ ((𝑗 = 𝑥 ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
170 | 28, 169 | prodeq12dv 11477 |
. . . 4
⊢ (𝑗 = 𝑥 → ∏𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐸 = ∏𝑦 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
171 | 167, 170 | syl5eq 2202 |
. . 3
⊢ (𝑗 = 𝑥 → ∏𝑘 ∈ 𝐵 𝐸 = ∏𝑦 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
172 | 160, 163,
171 | cbvprodi 11468 |
. 2
⊢
∏𝑗 ∈
𝐴 ∏𝑘 ∈ 𝐵 𝐸 = ∏𝑥 ∈ 𝐴 ∏𝑦 ∈ ⦋ 𝑥 / 𝑗⦌𝐵⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 |
173 | | nfcv 2299 |
. . 3
⊢
Ⅎ𝑦∏𝑗 ∈ 𝐷 𝐸 |
174 | 33, 119 | nfcprod 11463 |
. . 3
⊢
Ⅎ𝑘∏𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 |
175 | | nfcv 2299 |
. . . . 5
⊢
Ⅎ𝑥𝐸 |
176 | 175, 111,
114 | cbvprodi 11468 |
. . . 4
⊢
∏𝑗 ∈
𝐷 𝐸 = ∏𝑥 ∈ 𝐷 ⦋𝑥 / 𝑗⦌𝐸 |
177 | 121 | adantr 274 |
. . . . 5
⊢ ((𝑘 = 𝑦 ∧ 𝑥 ∈ 𝐷) → ⦋𝑥 / 𝑗⦌𝐸 = ⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
178 | 36, 177 | prodeq12dv 11477 |
. . . 4
⊢ (𝑘 = 𝑦 → ∏𝑥 ∈ 𝐷 ⦋𝑥 / 𝑗⦌𝐸 = ∏𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
179 | 176, 178 | syl5eq 2202 |
. . 3
⊢ (𝑘 = 𝑦 → ∏𝑗 ∈ 𝐷 𝐸 = ∏𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸) |
180 | 173, 174,
179 | cbvprodi 11468 |
. 2
⊢
∏𝑘 ∈
𝐶 ∏𝑗 ∈ 𝐷 𝐸 = ∏𝑦 ∈ 𝐶 ∏𝑥 ∈ ⦋ 𝑦 / 𝑘⦌𝐷⦋𝑦 / 𝑘⦌⦋𝑥 / 𝑗⦌𝐸 |
181 | 159, 172,
180 | 3eqtr4g 2215 |
1
⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐸 = ∏𝑘 ∈ 𝐶 ∏𝑗 ∈ 𝐷 𝐸) |