Step | Hyp | Ref
| Expression |
1 | | csbeq1a 3846 |
. . . 4
⊢ (𝑥 = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 →
𝐵 =
⦋〈(2nd ‘𝑦), (1st ‘𝑦)〉 / 𝑥⦌𝐵) |
2 | | fvex 6787 |
. . . . 5
⊢
(2nd ‘𝑦) ∈ V |
3 | | fvex 6787 |
. . . . 5
⊢
(1st ‘𝑦) ∈ V |
4 | | opex 5379 |
. . . . . . 7
⊢
〈𝑗, 𝑘〉 ∈ V |
5 | | fprodcnv.1 |
. . . . . . 7
⊢ (𝑥 = 〈𝑗, 𝑘〉 → 𝐵 = 𝐷) |
6 | 4, 5 | csbie 3868 |
. . . . . 6
⊢
⦋〈𝑗, 𝑘〉 / 𝑥⦌𝐵 = 𝐷 |
7 | | opeq12 4806 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 〈𝑗, 𝑘〉 = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
8 | 7 | csbeq1d 3836 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋〈𝑗, 𝑘〉 / 𝑥⦌𝐵 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵) |
9 | 6, 8 | eqtr3id 2792 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵) |
10 | 2, 3, 9 | csbie2 3874 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵 |
11 | 1, 10 | eqtr4di 2796 |
. . 3
⊢ (𝑥 = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 →
𝐵 =
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
12 | | fprodcnv.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
13 | | cnvfi 8963 |
. . . 4
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin) |
14 | 12, 13 | syl 17 |
. . 3
⊢ (𝜑 → ◡𝐴 ∈ Fin) |
15 | | relcnv 6012 |
. . . . 5
⊢ Rel ◡𝐴 |
16 | | cnvf1o 7951 |
. . . . 5
⊢ (Rel
◡𝐴 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴) |
17 | 15, 16 | ax-mp 5 |
. . . 4
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 |
18 | | fprodcnv.4 |
. . . . . 6
⊢ (𝜑 → Rel 𝐴) |
19 | | dfrel2 6092 |
. . . . . 6
⊢ (Rel
𝐴 ↔ ◡◡𝐴 = 𝐴) |
20 | 18, 19 | sylib 217 |
. . . . 5
⊢ (𝜑 → ◡◡𝐴 = 𝐴) |
21 | 20 | f1oeq3d 6713 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 ↔ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴)) |
22 | 17, 21 | mpbii 232 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴) |
23 | | 1st2nd 7880 |
. . . . . . 7
⊢ ((Rel
◡𝐴 ∧ 𝑦 ∈ ◡𝐴) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
24 | 15, 23 | mpan 687 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
25 | 24 | fveq2d 6778 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
26 | 24 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑦 ∈ ◡𝐴 → (𝑦 ∈ ◡𝐴 ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴)) |
27 | 26 | ibi 266 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴) |
28 | | sneq 4571 |
. . . . . . . . . 10
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
{𝑧} =
{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
29 | 28 | cnveqd 5784 |
. . . . . . . . 9
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
◡{𝑧} = ◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
30 | 29 | unieqd 4853 |
. . . . . . . 8
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
∪ ◡{𝑧} = ∪
◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
31 | | opswap 6132 |
. . . . . . . 8
⊢ ∪ ◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉} = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 |
32 | 30, 31 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
∪ ◡{𝑧} = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
33 | | eqid 2738 |
. . . . . . 7
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) |
34 | | opex 5379 |
. . . . . . 7
⊢
〈(2nd ‘𝑦), (1st ‘𝑦)〉 ∈ V |
35 | 32, 33, 34 | fvmpt 6875 |
. . . . . 6
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
36 | 27, 35 | syl 17 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
37 | 25, 36 | eqtrd 2778 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
38 | 37 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ◡𝐴) → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
39 | | fprodcnv.5 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
40 | 11, 14, 22, 38, 39 | fprodf1o 15656 |
. 2
⊢ (𝜑 → ∏𝑥 ∈ 𝐴 𝐵 = ∏𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
41 | | csbeq1a 3846 |
. . . . 5
⊢ (𝑦 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
𝐶 =
⦋〈(1st ‘𝑦), (2nd ‘𝑦)〉 / 𝑦⦌𝐶) |
42 | 24, 41 | syl 17 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
43 | | opex 5379 |
. . . . . . 7
⊢
〈𝑘, 𝑗〉 ∈ V |
44 | | fprodcnv.2 |
. . . . . . 7
⊢ (𝑦 = 〈𝑘, 𝑗〉 → 𝐶 = 𝐷) |
45 | 43, 44 | csbie 3868 |
. . . . . 6
⊢
⦋〈𝑘, 𝑗〉 / 𝑦⦌𝐶 = 𝐷 |
46 | | opeq12 4806 |
. . . . . . . 8
⊢ ((𝑘 = (1st ‘𝑦) ∧ 𝑗 = (2nd ‘𝑦)) → 〈𝑘, 𝑗〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
47 | 46 | ancoms 459 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 〈𝑘, 𝑗〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
48 | 47 | csbeq1d 3836 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋〈𝑘, 𝑗〉 / 𝑦⦌𝐶 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
49 | 45, 48 | eqtr3id 2792 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
50 | 2, 3, 49 | csbie2 3874 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶 |
51 | 42, 50 | eqtr4di 2796 |
. . 3
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋(2nd
‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
52 | 51 | prodeq2i 15629 |
. 2
⊢
∏𝑦 ∈
◡ 𝐴𝐶 = ∏𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 |
53 | 40, 52 | eqtr4di 2796 |
1
⊢ (𝜑 → ∏𝑥 ∈ 𝐴 𝐵 = ∏𝑦 ∈ ◡ 𝐴𝐶) |