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 4908 |
. . . . . 6
⊢ {𝑗} ∈ V |
6 | | gsum2d2.r |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
7 | | xpexg 6960 |
. . . . . 6
⊢ (({𝑗} ∈ V ∧ 𝐶 ∈ 𝑊) → ({𝑗} × 𝐶) ∈ V) |
8 | 5, 6, 7 | sylancr 695 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐶) ∈ V) |
9 | 8 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
10 | | iunexg 7143 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
11 | 4, 9, 10 | syl2anc 693 |
. . 3
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
12 | | gsum2d2.f |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) |
13 | 12 | ralrimivva 2971 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵) |
14 | | eqid 2622 |
. . . . 5
⊢ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
15 | 14 | fmpt2x 7236 |
. . . 4
⊢
(∀𝑗 ∈
𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
16 | 13, 15 | sylib 208 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
17 | | gsum2d2.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Fin) |
18 | | gsum2d2.n |
. . . 4
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) |
19 | 1, 2, 3, 4, 6, 12,
17, 18 | gsum2d2lem 18372 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ) |
20 | | relxp 5227 |
. . . . . . 7
⊢ Rel
({𝑘} × 𝐸) |
21 | 20 | rgenw 2924 |
. . . . . 6
⊢
∀𝑘 ∈
𝐷 Rel ({𝑘} × 𝐸) |
22 | | reliun 5239 |
. . . . . 6
⊢ (Rel
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ ∀𝑘 ∈ 𝐷 Rel ({𝑘} × 𝐸)) |
23 | 21, 22 | mpbir 221 |
. . . . 5
⊢ Rel
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
24 | | cnvf1o 7276 |
. . . . 5
⊢ (Rel
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
26 | | relxp 5227 |
. . . . . . . 8
⊢ Rel
({𝑗} × 𝐶) |
27 | 26 | rgenw 2924 |
. . . . . . 7
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐶) |
28 | | reliun 5239 |
. . . . . . 7
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶)) |
29 | 27, 28 | mpbir 221 |
. . . . . 6
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
30 | | relcnv 5503 |
. . . . . 6
⊢ Rel ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
31 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑘𝜑 |
32 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑘〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
33 | | nfiu1 4550 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
34 | 33 | nfcnv 5301 |
. . . . . . . . . 10
⊢
Ⅎ𝑘◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
35 | 34 | nfel2 2781 |
. . . . . . . . 9
⊢
Ⅎ𝑘〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
36 | 32, 35 | nfbi 1833 |
. . . . . . . 8
⊢
Ⅎ𝑘(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
37 | 31, 36 | nfim 1825 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
38 | | opeq2 4403 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → 〈𝑥, 𝑘〉 = 〈𝑥, 𝑦〉) |
39 | 38 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶))) |
40 | 38 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
41 | 39, 40 | bibi12d 335 |
. . . . . . . 8
⊢ (𝑘 = 𝑦 → ((〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) ↔ (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)))) |
42 | 41 | imbi2d 330 |
. . . . . . 7
⊢ (𝑘 = 𝑦 → ((𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) ↔ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))))) |
43 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
44 | | nfiu1 4550 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
45 | 44 | nfel2 2781 |
. . . . . . . . . 10
⊢
Ⅎ𝑗〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
46 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑗〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) |
47 | 45, 46 | nfbi 1833 |
. . . . . . . . 9
⊢
Ⅎ𝑗(〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
48 | 43, 47 | nfim 1825 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
49 | | opeq1 4402 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑥 → 〈𝑗, 𝑘〉 = 〈𝑥, 𝑘〉) |
50 | 49 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑥 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶))) |
51 | 49 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑥 → (〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
52 | 50, 51 | bibi12d 335 |
. . . . . . . . 9
⊢ (𝑗 = 𝑥 → ((〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) ↔ (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)))) |
53 | 52 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑗 = 𝑥 → ((𝜑 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) ↔ (𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))))) |
54 | | gsumcom2.c |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ↔ (𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸))) |
55 | | opeliunxp 5170 |
. . . . . . . . . 10
⊢
(〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
56 | | opeliunxp 5170 |
. . . . . . . . . 10
⊢
(〈𝑘, 𝑗〉 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ (𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸)) |
57 | 54, 55, 56 | 3bitr4g 303 |
. . . . . . . . 9
⊢ (𝜑 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑘, 𝑗〉 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
58 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑗 ∈ V |
59 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑘 ∈ V |
60 | 58, 59 | opelcnv 5304 |
. . . . . . . . 9
⊢
(〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↔ 〈𝑘, 𝑗〉 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
61 | 57, 60 | syl6bbr 278 |
. . . . . . . 8
⊢ (𝜑 → (〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑗, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
62 | 48, 53, 61 | chvar 2262 |
. . . . . . 7
⊢ (𝜑 → (〈𝑥, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑘〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
63 | 37, 42, 62 | chvar 2262 |
. . . . . 6
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
64 | 29, 30, 63 | eqrelrdv 5216 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) = ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)) |
65 | | f1oeq3 6129 |
. . . . 5
⊢ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) = ◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) → ((𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
66 | 64, 65 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→◡∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸))) |
67 | 25, 66 | mpbiri 248 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
68 | 1, 2, 3, 11, 16, 19, 67 | gsumf1o 18317 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})))) |
69 | | sneq 4187 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → {𝑧} = {〈𝑥, 𝑦〉}) |
70 | 69 | cnveqd 5298 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ◡{𝑧} = ◡{〈𝑥, 𝑦〉}) |
71 | 70 | unieqd 4446 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ∪
◡{𝑧} = ∪ ◡{〈𝑥, 𝑦〉}) |
72 | | opswap 5622 |
. . . . . . . . 9
⊢ ∪ ◡{〈𝑥, 𝑦〉} = 〈𝑦, 𝑥〉 |
73 | 71, 72 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ∪
◡{𝑧} = 〈𝑦, 𝑥〉) |
74 | 73 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧}) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑦, 𝑥〉)) |
75 | | df-ov 6653 |
. . . . . . 7
⊢ (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘〈𝑦, 𝑥〉) |
76 | 74, 75 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧}) = (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
77 | 76 | mpt2mptx 6751 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) = (𝑥 ∈ 𝐷, 𝑦 ∈ ⦋𝑥 / 𝑘⦌𝐸 ↦ (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
78 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥({𝑘} × 𝐸) |
79 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑘{𝑥} |
80 | | nfcsb1v 3549 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑥 / 𝑘⦌𝐸 |
81 | 79, 80 | nfxp 5142 |
. . . . . . 7
⊢
Ⅎ𝑘({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) |
82 | | sneq 4187 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → {𝑘} = {𝑥}) |
83 | | csbeq1a 3542 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → 𝐸 = ⦋𝑥 / 𝑘⦌𝐸) |
84 | 82, 83 | xpeq12d 5140 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → ({𝑘} × 𝐸) = ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸)) |
85 | 78, 81, 84 | cbviun 4557 |
. . . . . 6
⊢ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) = ∪
𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) |
86 | | mpteq1 4737 |
. . . . . 6
⊢ (∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) = ∪
𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) = (𝑧 ∈ ∪
𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧}))) |
87 | 85, 86 | ax-mp 5 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) = (𝑧 ∈ ∪
𝑥 ∈ 𝐷 ({𝑥} × ⦋𝑥 / 𝑘⦌𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) |
88 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥𝐸 |
89 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) |
90 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑦(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) |
91 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑘𝑦 |
92 | | nfmpt22 6723 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
93 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑘𝑥 |
94 | 91, 92, 93 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑘(𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) |
95 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑗𝑦 |
96 | | nfmpt21 6722 |
. . . . . . 7
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
97 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑗𝑥 |
98 | 95, 96, 97 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑗(𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) |
99 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
100 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑗 = 𝑦 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥) = (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
101 | 99, 100 | sylan9eq 2676 |
. . . . . 6
⊢ ((𝑘 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
102 | 88, 80, 89, 90, 94, 98, 83, 101 | cbvmpt2x 6733 |
. . . . 5
⊢ (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) = (𝑥 ∈ 𝐷, 𝑦 ∈ ⦋𝑥 / 𝑘⦌𝐸 ↦ (𝑦(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑥)) |
103 | 77, 87, 102 | 3eqtr4i 2654 |
. . . 4
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) = (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
104 | | f1of 6137 |
. . . . . . 7
⊢ ((𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)–1-1-onto→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
105 | 67, 104 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
106 | | eqid 2622 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}) |
107 | 106 | fmpt 6381 |
. . . . . 6
⊢
(∀𝑧 ∈
∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)∪ ◡{𝑧} ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}):∪ 𝑘 ∈ 𝐷 ({𝑘} × 𝐸)⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
108 | 105, 107 | sylibr 224 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸)∪ ◡{𝑧} ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
109 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}) = (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})) |
110 | 16 | feqmptd 6249 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑥 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑥))) |
111 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = ∪
◡{𝑧} → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘𝑥) = ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧})) |
112 | 108, 109,
110, 111 | fmptcof 6397 |
. . . 4
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})) = (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)‘∪ ◡{𝑧}))) |
113 | 12 | ex 450 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → 𝑋 ∈ 𝐵)) |
114 | 14 | ovmpt4g 6783 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
115 | 114 | 3expia 1267 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑋 ∈ 𝐵 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)) |
116 | 113, 115 | sylcom 30 |
. . . . . . . 8
⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)) |
117 | 54, 116 | sylbird 250 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋)) |
118 | 117 | 3impib 1262 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
119 | 118 | eqcomd 2628 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸) → 𝑋 = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
120 | 119 | mpt2eq3dva 6719 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋) = (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘))) |
121 | 103, 112,
120 | 3eqtr4a 2682 |
. . 3
⊢ (𝜑 → ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧})) = (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋)) |
122 | 121 | oveq2d 6666 |
. 2
⊢ (𝜑 → (𝐺 Σg ((𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) ∘ (𝑧 ∈ ∪
𝑘 ∈ 𝐷 ({𝑘} × 𝐸) ↦ ∪ ◡{𝑧}))) = (𝐺 Σg (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋))) |
123 | 68, 122 | eqtrd 2656 |
1
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋))) |