Step | Hyp | Ref
| Expression |
1 | | gsum2d2.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsum2d2.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
3 | | gsum2d2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) |
4 | | gsum2d2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | snex 5324 |
. . . . . 6
⊢ {𝑗} ∈ V |
6 | | gsum2d2.r |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
7 | | xpexg 7535 |
. . . . . 6
⊢ (({𝑗} ∈ V ∧ 𝐶 ∈ 𝑊) → ({𝑗} × 𝐶) ∈ V) |
8 | 5, 6, 7 | sylancr 590 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐶) ∈ V) |
9 | 8 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
10 | | iunexg 7736 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
11 | 4, 9, 10 | syl2anc 587 |
. . 3
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
12 | | gsum2d2.f |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) |
13 | 12 | ralrimivva 3112 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵) |
14 | | eqid 2737 |
. . . . 5
⊢ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
15 | 14 | fmpox 7837 |
. . . 4
⊢
(∀𝑗 ∈
𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
16 | 13, 15 | sylib 221 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
17 | | gsum2d2.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Fin) |
18 | | gsum2d2.n |
. . . 4
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) |
19 | 1, 2, 3, 4, 6, 12,
17, 18 | gsum2d2lem 19358 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ) |
20 | | relxp 5569 |
. . . . . . 7
⊢ Rel
({𝑘} × 𝐸) |
21 | 20 | rgenw 3073 |
. . . . . 6
⊢
∀𝑘 ∈
𝐷 Rel ({𝑘} × 𝐸) |
22 | | reliun 5686 |
. . . . . 6
⊢ (Rel
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ ∀𝑘 ∈ 𝐷 Rel ({𝑘} × 𝐸)) |
23 | 21, 22 | mpbir 234 |
. . . . 5
⊢ Rel
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
24 | | cnvf1o 7879 |
. . . . 5
⊢ (Rel
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
26 | | relxp 5569 |
. . . . . . . 8
⊢ Rel
({𝑗} × 𝐶) |
27 | 26 | rgenw 3073 |
. . . . . . 7
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐶) |
28 | | reliun 5686 |
. . . . . . 7
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶)) |
29 | 27, 28 | mpbir 234 |
. . . . . 6
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
30 | | relcnv 5972 |
. . . . . 6
⊢ Rel ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
31 | | nfv 1922 |
. . . . . . . 8
⊢
Ⅎ𝑘𝜑 |
32 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑘〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
33 | | nfiu1 4938 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
34 | 33 | nfcnv 5747 |
. . . . . . . . . 10
⊢
Ⅎ𝑘◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
35 | 34 | nfel2 2922 |
. . . . . . . . 9
⊢
Ⅎ𝑘〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
36 | 32, 35 | nfbi 1911 |
. . . . . . . 8
⊢
Ⅎ𝑘(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
37 | 31, 36 | nfim 1904 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
38 | | opeq2 4785 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → 〈𝑥, 𝑘〉 = 〈𝑥, 𝑦〉) |
39 | 38 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶))) |
40 | 38 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
41 | 39, 40 | bibi12d 349 |
. . . . . . . 8
⊢ (𝑘 = 𝑦 → ((〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) ↔ (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)))) |
42 | 41 | imbi2d 344 |
. . . . . . 7
⊢ (𝑘 = 𝑦 → ((𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) ↔ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))))) |
43 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
44 | | nfiu1 4938 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
45 | 44 | nfel2 2922 |
. . . . . . . . . 10
⊢
Ⅎ𝑗〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
46 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑗〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
47 | 45, 46 | nfbi 1911 |
. . . . . . . . 9
⊢
Ⅎ𝑗(〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
48 | 43, 47 | nfim 1904 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
49 | | opeq1 4784 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑥 → 〈𝑗, 𝑘〉 = 〈𝑥, 𝑘〉) |
50 | 49 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑥 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶))) |
51 | 49 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑥 → (〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
52 | 50, 51 | bibi12d 349 |
. . . . . . . . 9
⊢ (𝑗 = 𝑥 → ((〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) ↔ (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)))) |
53 | 52 | imbi2d 344 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → ((𝜑 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) ↔ (𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))))) |
54 | | gsumcom2.c |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ↔ (𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸))) |
55 | | opeliunxp 5616 |
. . . . . . . . . 10
⊢
(〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
56 | | opeliunxp 5616 |
. . . . . . . . . 10
⊢
(〈𝑘, 𝑗〉 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ (𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸)) |
57 | 54, 55, 56 | 3bitr4g 317 |
. . . . . . . . 9
⊢ (𝜑 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑘, 𝑗〉 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
58 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑗 ∈ V |
59 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑘 ∈ V |
60 | 58, 59 | opelcnv 5750 |
. . . . . . . . 9
⊢
(〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ 〈𝑘, 𝑗〉 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
61 | 57, 60 | bitr4di 292 |
. . . . . . . 8
⊢ (𝜑 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
62 | 48, 53, 61 | chvarfv 2238 |
. . . . . . 7
⊢ (𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
63 | 37, 42, 62 | chvarfv 2238 |
. . . . . 6
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
64 | 29, 30, 63 | eqrelrdv 5662 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) = ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
65 | 64 | f1oeq3d 6658 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
66 | 25, 65 | mpbiri 261 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
67 | 1, 2, 3, 11, 16, 19, 66 | gsumf1o 19301 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})))) |
68 | | sneq 4551 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → {𝑧} = {〈𝑥, 𝑦〉}) |
69 | 68 | cnveqd 5744 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ◡{𝑧} = ◡{〈𝑥, 𝑦〉}) |
70 | 69 | unieqd 4833 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ∪
◡{𝑧} = ∪ ◡{〈𝑥, 𝑦〉}) |
71 | | opswap 6092 |
. . . . . . . . 9
⊢ ∪ ◡{〈𝑥, 𝑦〉} = 〈𝑦, 𝑥〉 |
72 | 70, 71 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ∪
◡{𝑧} = 〈𝑦, 𝑥〉) |
73 | 72 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧}) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑦, 𝑥〉)) |
74 | | df-ov 7216 |
. . . . . . 7
⊢ (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑦, 𝑥〉) |
75 | 73, 74 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧}) = (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
76 | 75 | mpomptx 7323 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) = (𝑥 ∈ 𝐷, 𝑦 ∈ ⦋𝑥 / 𝑘⦌𝐸 ↦ (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
77 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥({𝑘} × 𝐸) |
78 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑘{𝑥} |
79 | | nfcsb1v 3836 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐸 |
80 | 78, 79 | nfxp 5584 |
. . . . . . 7
⊢
Ⅎ𝑘({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) |
81 | | sneq 4551 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → {𝑘} = {𝑥}) |
82 | | csbeq1a 3825 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → 𝐸 = ⦋𝑥 / 𝑘⦌𝐸) |
83 | 81, 82 | xpeq12d 5582 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → ({𝑘} × 𝐸) = ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸)) |
84 | 77, 80, 83 | cbviun 4945 |
. . . . . 6
⊢ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) = ∪
𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) |
85 | 84 | mpteq1i 5145 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) = (𝑧 ∈ ∪
𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) |
86 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥𝐸 |
87 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) |
88 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑦(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) |
89 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑘𝑦 |
90 | | nfmpo2 7292 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
91 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑘𝑥 |
92 | 89, 90, 91 | nfov 7243 |
. . . . . 6
⊢
Ⅎ𝑘(𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) |
93 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑗𝑦 |
94 | | nfmpo1 7291 |
. . . . . . 7
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
95 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑗𝑥 |
96 | 93, 94, 95 | nfov 7243 |
. . . . . 6
⊢
Ⅎ𝑗(𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) |
97 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
98 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑗 = 𝑦 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) = (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
99 | 97, 98 | sylan9eq 2798 |
. . . . . 6
⊢ ((𝑘 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
100 | 86, 79, 87, 88, 92, 96, 82, 99 | cbvmpox 7304 |
. . . . 5
⊢ (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) = (𝑥 ∈ 𝐷, 𝑦 ∈ ⦋𝑥 / 𝑘⦌𝐸 ↦ (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
101 | 76, 85, 100 | 3eqtr4i 2775 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) = (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
102 | | f1of 6661 |
. . . . . . 7
⊢ ((𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
103 | 66, 102 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
104 | | eqid 2737 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}) |
105 | 104 | fmpt 6927 |
. . . . . 6
⊢
(∀𝑧 ∈
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)∪ ◡{𝑧} ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
106 | 103, 105 | sylibr 237 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸)∪ ◡{𝑧} ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
107 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})) |
108 | 16 | feqmptd 6780 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑥 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑥))) |
109 | | fveq2 6717 |
. . . . 5
⊢ (𝑥 = ∪
◡{𝑧} → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑥) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) |
110 | 106, 107,
108, 109 | fmptcof 6945 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})) = (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧}))) |
111 | 12 | ex 416 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → 𝑋 ∈ 𝐵)) |
112 | 14 | ovmpt4g 7356 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
113 | 112 | 3expia 1123 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑋 ∈ 𝐵 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)) |
114 | 111, 113 | sylcom 30 |
. . . . . . . 8
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)) |
115 | 54, 114 | sylbird 263 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)) |
116 | 115 | 3impib 1118 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
117 | 116 | eqcomd 2743 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸) → 𝑋 = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
118 | 117 | mpoeq3dva 7288 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋) = (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘))) |
119 | 101, 110,
118 | 3eqtr4a 2804 |
. . 3
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})) = (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋)) |
120 | 119 | oveq2d 7229 |
. 2
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}))) = (𝐺 Σg (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋))) |
121 | 67, 120 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋))) |