Step | Hyp | Ref
| Expression |
1 | | csbeq1a 3058 |
. . . 4
⊢ (𝑥 = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 →
𝐵 =
⦋〈(2nd ‘𝑦), (1st ‘𝑦)〉 / 𝑥⦌𝐵) |
2 | | 2ndexg 6147 |
. . . . . 6
⊢ (𝑦 ∈ V → (2nd
‘𝑦) ∈
V) |
3 | 2 | elv 2734 |
. . . . 5
⊢
(2nd ‘𝑦) ∈ V |
4 | | 1stexg 6146 |
. . . . . 6
⊢ (𝑦 ∈ V → (1st
‘𝑦) ∈
V) |
5 | 4 | elv 2734 |
. . . . 5
⊢
(1st ‘𝑦) ∈ V |
6 | | vex 2733 |
. . . . . . . 8
⊢ 𝑗 ∈ V |
7 | | vex 2733 |
. . . . . . . 8
⊢ 𝑘 ∈ V |
8 | 6, 7 | opex 4214 |
. . . . . . 7
⊢
〈𝑗, 𝑘〉 ∈ V |
9 | | fprodcnv.1 |
. . . . . . 7
⊢ (𝑥 = 〈𝑗, 𝑘〉 → 𝐵 = 𝐷) |
10 | 8, 9 | csbie 3094 |
. . . . . 6
⊢
⦋〈𝑗, 𝑘〉 / 𝑥⦌𝐵 = 𝐷 |
11 | | opeq12 3767 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 〈𝑗, 𝑘〉 = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
12 | 11 | csbeq1d 3056 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋〈𝑗, 𝑘〉 / 𝑥⦌𝐵 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵) |
13 | 10, 12 | eqtr3id 2217 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵) |
14 | 3, 5, 13 | csbie2 3098 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋〈(2nd
‘𝑦), (1st
‘𝑦)〉 / 𝑥⦌𝐵 |
15 | 1, 14 | eqtr4di 2221 |
. . 3
⊢ (𝑥 = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 →
𝐵 =
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
16 | | fprodcnv.4 |
. . . 4
⊢ (𝜑 → Rel 𝐴) |
17 | | fprodcnv.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
18 | | relcnvfi 6918 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐴 ∈ Fin) → ◡𝐴 ∈ Fin) |
19 | 16, 17, 18 | syl2anc 409 |
. . 3
⊢ (𝜑 → ◡𝐴 ∈ Fin) |
20 | | relcnv 4989 |
. . . . 5
⊢ Rel ◡𝐴 |
21 | | cnvf1o 6204 |
. . . . 5
⊢ (Rel
◡𝐴 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴) |
22 | 20, 21 | ax-mp 5 |
. . . 4
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 |
23 | | dfrel2 5061 |
. . . . . 6
⊢ (Rel
𝐴 ↔ ◡◡𝐴 = 𝐴) |
24 | 16, 23 | sylib 121 |
. . . . 5
⊢ (𝜑 → ◡◡𝐴 = 𝐴) |
25 | 24 | f1oeq3d 5439 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→◡◡𝐴 ↔ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴)) |
26 | 22, 25 | mpbii 147 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}):◡𝐴–1-1-onto→𝐴) |
27 | | 1st2nd 6160 |
. . . . . . 7
⊢ ((Rel
◡𝐴 ∧ 𝑦 ∈ ◡𝐴) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
28 | 20, 27 | mpan 422 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
29 | 28 | fveq2d 5500 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
30 | 28 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑦 ∈ ◡𝐴 → (𝑦 ∈ ◡𝐴 ↔ 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴)) |
31 | 30 | ibi 175 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝐴 → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴) |
32 | | sneq 3594 |
. . . . . . . . . 10
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
{𝑧} =
{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
33 | 32 | cnveqd 4787 |
. . . . . . . . 9
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
◡{𝑧} = ◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
34 | 33 | unieqd 3807 |
. . . . . . . 8
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
∪ ◡{𝑧} = ∪
◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉}) |
35 | | opswapg 5097 |
. . . . . . . . 9
⊢
(((1st ‘𝑦) ∈ V ∧ (2nd ‘𝑦) ∈ V) → ∪ ◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉} = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
36 | 5, 3, 35 | mp2an 424 |
. . . . . . . 8
⊢ ∪ ◡{〈(1st ‘𝑦), (2nd ‘𝑦)〉} = 〈(2nd
‘𝑦), (1st
‘𝑦)〉 |
37 | 34, 36 | eqtrdi 2219 |
. . . . . . 7
⊢ (𝑧 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
∪ ◡{𝑧} = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
38 | | eqid 2170 |
. . . . . . 7
⊢ (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧}) |
39 | 3, 5 | opex 4214 |
. . . . . . 7
⊢
〈(2nd ‘𝑦), (1st ‘𝑦)〉 ∈ V |
40 | 37, 38, 39 | fvmpt 5573 |
. . . . . 6
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
41 | 31, 40 | syl 14 |
. . . . 5
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) = 〈(2nd
‘𝑦), (1st
‘𝑦)〉) |
42 | 29, 41 | eqtrd 2203 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
43 | 42 | adantl 275 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ◡𝐴) → ((𝑧 ∈ ◡𝐴 ↦ ∪ ◡{𝑧})‘𝑦) = 〈(2nd ‘𝑦), (1st ‘𝑦)〉) |
44 | | fprodcnv.5 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
45 | 15, 19, 26, 43, 44 | fprodf1o 11551 |
. 2
⊢ (𝜑 → ∏𝑥 ∈ 𝐴 𝐵 = ∏𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
46 | | csbeq1a 3058 |
. . . . 5
⊢ (𝑦 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉 →
𝐶 =
⦋〈(1st ‘𝑦), (2nd ‘𝑦)〉 / 𝑦⦌𝐶) |
47 | 28, 46 | syl 14 |
. . . 4
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
48 | 7, 6 | opex 4214 |
. . . . . . 7
⊢
〈𝑘, 𝑗〉 ∈ V |
49 | | fprodcnv.2 |
. . . . . . 7
⊢ (𝑦 = 〈𝑘, 𝑗〉 → 𝐶 = 𝐷) |
50 | 48, 49 | csbie 3094 |
. . . . . 6
⊢
⦋〈𝑘, 𝑗〉 / 𝑦⦌𝐶 = 𝐷 |
51 | | opeq12 3767 |
. . . . . . . 8
⊢ ((𝑘 = (1st ‘𝑦) ∧ 𝑗 = (2nd ‘𝑦)) → 〈𝑘, 𝑗〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
52 | 51 | ancoms 266 |
. . . . . . 7
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 〈𝑘, 𝑗〉 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
53 | 52 | csbeq1d 3056 |
. . . . . 6
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → ⦋〈𝑘, 𝑗〉 / 𝑦⦌𝐶 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
54 | 50, 53 | eqtr3id 2217 |
. . . . 5
⊢ ((𝑗 = (2nd ‘𝑦) ∧ 𝑘 = (1st ‘𝑦)) → 𝐷 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶) |
55 | 3, 5, 54 | csbie2 3098 |
. . . 4
⊢
⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 = ⦋〈(1st
‘𝑦), (2nd
‘𝑦)〉 / 𝑦⦌𝐶 |
56 | 47, 55 | eqtr4di 2221 |
. . 3
⊢ (𝑦 ∈ ◡𝐴 → 𝐶 = ⦋(2nd
‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷) |
57 | 56 | prodeq2i 11525 |
. 2
⊢
∏𝑦 ∈
◡ 𝐴𝐶 = ∏𝑦 ∈ ◡ 𝐴⦋(2nd ‘𝑦) / 𝑗⦌⦋(1st
‘𝑦) / 𝑘⦌𝐷 |
58 | 45, 57 | eqtr4di 2221 |
1
⊢ (𝜑 → ∏𝑥 ∈ 𝐴 𝐵 = ∏𝑦 ∈ ◡ 𝐴𝐶) |