# Metamath Proof Explorer

## Theorem gsumcom2

Description: Two-dimensional commutation of a group sum. Note that while A and D are constants w.r.t. j , k , C ( j ) and E ( k ) are not. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses gsum2d2.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsum2d2.z
gsum2d2.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsum2d2.a ${⊢}{\phi }\to {A}\in {V}$
gsum2d2.r ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {C}\in {W}$
gsum2d2.f ${⊢}\left({\phi }\wedge \left({j}\in {A}\wedge {k}\in {C}\right)\right)\to {X}\in {B}$
gsum2d2.u ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
gsum2d2.n
gsumcom2.d ${⊢}{\phi }\to {D}\in {Y}$
gsumcom2.c ${⊢}{\phi }\to \left(\left({j}\in {A}\wedge {k}\in {C}\right)↔\left({k}\in {D}\wedge {j}\in {E}\right)\right)$
Assertion gsumcom2 ${⊢}{\phi }\to {\sum }_{{G}}\left({j}\in {A},{k}\in {C}⟼{X}\right)={\sum }_{{G}}\left({k}\in {D},{j}\in {E}⟼{X}\right)$

### Proof

Step Hyp Ref Expression
1 gsum2d2.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsum2d2.z
3 gsum2d2.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
4 gsum2d2.a ${⊢}{\phi }\to {A}\in {V}$
5 gsum2d2.r ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {C}\in {W}$
6 gsum2d2.f ${⊢}\left({\phi }\wedge \left({j}\in {A}\wedge {k}\in {C}\right)\right)\to {X}\in {B}$
7 gsum2d2.u ${⊢}{\phi }\to {U}\in \mathrm{Fin}$
8 gsum2d2.n
9 gsumcom2.d ${⊢}{\phi }\to {D}\in {Y}$
10 gsumcom2.c ${⊢}{\phi }\to \left(\left({j}\in {A}\wedge {k}\in {C}\right)↔\left({k}\in {D}\wedge {j}\in {E}\right)\right)$
11 snex ${⊢}\left\{{j}\right\}\in \mathrm{V}$
12 xpexg ${⊢}\left(\left\{{j}\right\}\in \mathrm{V}\wedge {C}\in {W}\right)\to \left\{{j}\right\}×{C}\in \mathrm{V}$
13 11 5 12 sylancr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left\{{j}\right\}×{C}\in \mathrm{V}$
14 13 ralrimiva ${⊢}{\phi }\to \forall {j}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{j}\right\}×{C}\in \mathrm{V}$
15 iunexg ${⊢}\left({A}\in {V}\wedge \forall {j}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{j}\right\}×{C}\in \mathrm{V}\right)\to \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)\in \mathrm{V}$
16 4 14 15 syl2anc ${⊢}{\phi }\to \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)\in \mathrm{V}$
17 6 ralrimivva ${⊢}{\phi }\to \forall {j}\in {A}\phantom{\rule{.4em}{0ex}}\forall {k}\in {C}\phantom{\rule{.4em}{0ex}}{X}\in {B}$
18 eqid ${⊢}\left({j}\in {A},{k}\in {C}⟼{X}\right)=\left({j}\in {A},{k}\in {C}⟼{X}\right)$
19 18 fmpox ${⊢}\forall {j}\in {A}\phantom{\rule{.4em}{0ex}}\forall {k}\in {C}\phantom{\rule{.4em}{0ex}}{X}\in {B}↔\left({j}\in {A},{k}\in {C}⟼{X}\right):\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)⟶{B}$
20 17 19 sylib ${⊢}{\phi }\to \left({j}\in {A},{k}\in {C}⟼{X}\right):\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)⟶{B}$
21 1 2 3 4 5 6 7 8 gsum2d2lem
22 relxp ${⊢}\mathrm{Rel}\left(\left\{{k}\right\}×{E}\right)$
23 22 rgenw ${⊢}\forall {k}\in {D}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}\left(\left\{{k}\right\}×{E}\right)$
24 reliun ${⊢}\mathrm{Rel}\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)↔\forall {k}\in {D}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}\left(\left\{{k}\right\}×{E}\right)$
25 23 24 mpbir ${⊢}\mathrm{Rel}\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)$
26 cnvf1o ${⊢}\mathrm{Rel}\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\to \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\underset{1-1 onto}{⟶}{\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}$
27 25 26 ax-mp ${⊢}\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\underset{1-1 onto}{⟶}{\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}$
28 relxp ${⊢}\mathrm{Rel}\left(\left\{{j}\right\}×{C}\right)$
29 28 rgenw ${⊢}\forall {j}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}\left(\left\{{j}\right\}×{C}\right)$
30 reliun ${⊢}\mathrm{Rel}\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔\forall {j}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}\left(\left\{{j}\right\}×{C}\right)$
31 29 30 mpbir ${⊢}\mathrm{Rel}\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
32 relcnv ${⊢}\mathrm{Rel}{\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}$
33 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
34 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
35 nfiu1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)$
36 35 nfcnv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}$
37 36 nfel2 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}$
38 34 37 nfbi ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{y}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
39 33 38 nfim ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left(⟨{x},{y}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{y}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)$
40 opeq2 ${⊢}{k}={y}\to ⟨{x},{k}⟩=⟨{x},{y}⟩$
41 40 eleq1d ${⊢}{k}={y}\to \left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{y}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)\right)$
42 40 eleq1d ${⊢}{k}={y}\to \left(⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}↔⟨{x},{y}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
43 41 42 bibi12d ${⊢}{k}={y}\to \left(\left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)↔\left(⟨{x},{y}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{y}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)$
44 43 imbi2d ${⊢}{k}={y}\to \left(\left({\phi }\to \left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)↔\left({\phi }\to \left(⟨{x},{y}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{y}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)\right)$
45 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
46 nfiu1 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
47 46 nfel2 ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
48 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}$
49 47 48 nfbi ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
50 45 49 nfim ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)$
51 opeq1 ${⊢}{j}={x}\to ⟨{j},{k}⟩=⟨{x},{k}⟩$
52 51 eleq1d ${⊢}{j}={x}\to \left(⟨{j},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)\right)$
53 51 eleq1d ${⊢}{j}={x}\to \left(⟨{j},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
54 52 53 bibi12d ${⊢}{j}={x}\to \left(\left(⟨{j},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{j},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)↔\left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)$
55 54 imbi2d ${⊢}{j}={x}\to \left(\left({\phi }\to \left(⟨{j},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{j},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)↔\left({\phi }\to \left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)\right)\right)$
56 opeliunxp ${⊢}⟨{j},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔\left({j}\in {A}\wedge {k}\in {C}\right)$
57 opeliunxp ${⊢}⟨{k},{j}⟩\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)↔\left({k}\in {D}\wedge {j}\in {E}\right)$
58 10 56 57 3bitr4g ${⊢}{\phi }\to \left(⟨{j},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{k},{j}⟩\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\right)$
59 vex ${⊢}{j}\in \mathrm{V}$
60 vex ${⊢}{k}\in \mathrm{V}$
61 59 60 opelcnv ${⊢}⟨{j},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}↔⟨{k},{j}⟩\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)$
62 58 61 syl6bbr ${⊢}{\phi }\to \left(⟨{j},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{j},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
63 50 55 62 chvarfv ${⊢}{\phi }\to \left(⟨{x},{k}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{k}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
64 39 44 63 chvarfv ${⊢}{\phi }\to \left(⟨{x},{y}⟩\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔⟨{x},{y}⟩\in {\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
65 31 32 64 eqrelrdv ${⊢}{\phi }\to \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)={\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}$
66 65 f1oeq3d ${⊢}{\phi }\to \left(\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\underset{1-1 onto}{⟶}\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\underset{1-1 onto}{⟶}{\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)}^{-1}\right)$
67 27 66 mpbiri ${⊢}{\phi }\to \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\underset{1-1 onto}{⟶}\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
68 1 2 3 16 20 21 67 gsumf1o ${⊢}{\phi }\to {\sum }_{{G}}\left({j}\in {A},{k}\in {C}⟼{X}\right)={\sum }_{{G}}\left(\left({j}\in {A},{k}\in {C}⟼{X}\right)\circ \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)\right)$
69 sneq ${⊢}{z}=⟨{x},{y}⟩\to \left\{{z}\right\}=\left\{⟨{x},{y}⟩\right\}$
70 69 cnveqd ${⊢}{z}=⟨{x},{y}⟩\to {\left\{{z}\right\}}^{-1}={\left\{⟨{x},{y}⟩\right\}}^{-1}$
71 70 unieqd ${⊢}{z}=⟨{x},{y}⟩\to \bigcup {\left\{{z}\right\}}^{-1}=\bigcup {\left\{⟨{x},{y}⟩\right\}}^{-1}$
72 opswap ${⊢}\bigcup {\left\{⟨{x},{y}⟩\right\}}^{-1}=⟨{y},{x}⟩$
73 71 72 syl6eq ${⊢}{z}=⟨{x},{y}⟩\to \bigcup {\left\{{z}\right\}}^{-1}=⟨{y},{x}⟩$
74 73 fveq2d ${⊢}{z}=⟨{x},{y}⟩\to \left({j}\in {A},{k}\in {C}⟼{X}\right)\left(\bigcup {\left\{{z}\right\}}^{-1}\right)=\left({j}\in {A},{k}\in {C}⟼{X}\right)\left(⟨{y},{x}⟩\right)$
75 df-ov ${⊢}{y}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}=\left({j}\in {A},{k}\in {C}⟼{X}\right)\left(⟨{y},{x}⟩\right)$
76 74 75 syl6eqr ${⊢}{z}=⟨{x},{y}⟩\to \left({j}\in {A},{k}\in {C}⟼{X}\right)\left(\bigcup {\left\{{z}\right\}}^{-1}\right)={y}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}$
77 76 mpomptx
78 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\left\{{k}\right\}×{E}\right)$
79 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left\{{x}\right\}$
80 nfcsb1v
81 79 80 nfxp
82 sneq ${⊢}{k}={x}\to \left\{{k}\right\}=\left\{{x}\right\}$
83 csbeq1a
84 82 83 xpeq12d
85 78 81 84 cbviun
86 85 mpteq1i
87 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{E}$
88 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}\right)$
89 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}\right)$
90 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{y}$
91 nfmpo2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({j}\in {A},{k}\in {C}⟼{X}\right)$
92 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{x}$
93 90 91 92 nfov ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({y}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}\right)$
94 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{y}$
95 nfmpo1 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}\left({j}\in {A},{k}\in {C}⟼{X}\right)$
96 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{x}$
97 94 95 96 nfov ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}\left({y}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}\right)$
98 oveq2 ${⊢}{k}={x}\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}={j}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}$
99 oveq1 ${⊢}{j}={y}\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}={y}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}$
100 98 99 sylan9eq ${⊢}\left({k}={x}\wedge {j}={y}\right)\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}={y}\left({j}\in {A},{k}\in {C}⟼{X}\right){x}$
101 87 80 88 89 93 97 83 100 cbvmpox
102 77 86 101 3eqtr4i ${⊢}\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\left({j}\in {A},{k}\in {C}⟼{X}\right)\left(\bigcup {\left\{{z}\right\}}^{-1}\right)\right)=\left({k}\in {D},{j}\in {E}⟼{j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}\right)$
103 f1of ${⊢}\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\underset{1-1 onto}{⟶}\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)\to \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟶\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
104 67 103 syl ${⊢}{\phi }\to \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟶\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
105 eqid ${⊢}\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)=\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)$
106 105 fmpt ${⊢}\forall {z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\phantom{\rule{.4em}{0ex}}\bigcup {\left\{{z}\right\}}^{-1}\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)↔\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right):\bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟶\bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
107 104 106 sylibr ${⊢}{\phi }\to \forall {z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)\phantom{\rule{.4em}{0ex}}\bigcup {\left\{{z}\right\}}^{-1}\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)$
108 eqidd ${⊢}{\phi }\to \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)=\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)$
109 20 feqmptd ${⊢}{\phi }\to \left({j}\in {A},{k}\in {C}⟼{X}\right)=\left({x}\in \bigcup _{{j}\in {A}}\left(\left\{{j}\right\}×{C}\right)⟼\left({j}\in {A},{k}\in {C}⟼{X}\right)\left({x}\right)\right)$
110 fveq2 ${⊢}{x}=\bigcup {\left\{{z}\right\}}^{-1}\to \left({j}\in {A},{k}\in {C}⟼{X}\right)\left({x}\right)=\left({j}\in {A},{k}\in {C}⟼{X}\right)\left(\bigcup {\left\{{z}\right\}}^{-1}\right)$
111 107 108 109 110 fmptcof ${⊢}{\phi }\to \left({j}\in {A},{k}\in {C}⟼{X}\right)\circ \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)=\left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\left({j}\in {A},{k}\in {C}⟼{X}\right)\left(\bigcup {\left\{{z}\right\}}^{-1}\right)\right)$
112 6 ex ${⊢}{\phi }\to \left(\left({j}\in {A}\wedge {k}\in {C}\right)\to {X}\in {B}\right)$
113 18 ovmpt4g ${⊢}\left({j}\in {A}\wedge {k}\in {C}\wedge {X}\in {B}\right)\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}={X}$
114 113 3expia ${⊢}\left({j}\in {A}\wedge {k}\in {C}\right)\to \left({X}\in {B}\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}={X}\right)$
115 112 114 sylcom ${⊢}{\phi }\to \left(\left({j}\in {A}\wedge {k}\in {C}\right)\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}={X}\right)$
116 10 115 sylbird ${⊢}{\phi }\to \left(\left({k}\in {D}\wedge {j}\in {E}\right)\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}={X}\right)$
117 116 3impib ${⊢}\left({\phi }\wedge {k}\in {D}\wedge {j}\in {E}\right)\to {j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}={X}$
118 117 eqcomd ${⊢}\left({\phi }\wedge {k}\in {D}\wedge {j}\in {E}\right)\to {X}={j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}$
119 118 mpoeq3dva ${⊢}{\phi }\to \left({k}\in {D},{j}\in {E}⟼{X}\right)=\left({k}\in {D},{j}\in {E}⟼{j}\left({j}\in {A},{k}\in {C}⟼{X}\right){k}\right)$
120 102 111 119 3eqtr4a ${⊢}{\phi }\to \left({j}\in {A},{k}\in {C}⟼{X}\right)\circ \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)=\left({k}\in {D},{j}\in {E}⟼{X}\right)$
121 120 oveq2d ${⊢}{\phi }\to {\sum }_{{G}}\left(\left({j}\in {A},{k}\in {C}⟼{X}\right)\circ \left({z}\in \bigcup _{{k}\in {D}}\left(\left\{{k}\right\}×{E}\right)⟼\bigcup {\left\{{z}\right\}}^{-1}\right)\right)={\sum }_{{G}}\left({k}\in {D},{j}\in {E}⟼{X}\right)$
122 68 121 eqtrd ${⊢}{\phi }\to {\sum }_{{G}}\left({j}\in {A},{k}\in {C}⟼{X}\right)={\sum }_{{G}}\left({k}\in {D},{j}\in {E}⟼{X}\right)$