Theorem esum2dlem

Description: Lemma for esum2d (finite case). (Contributed by Thierry Arnoux, 17-May-2020) (Proof shortened by AV, 17-Sep-2021)

	Ref	Expression
Hypotheses	esum2d.0	$$⊢\underset{\_}{Ⅎ}kF$$
	esum2d.1	$$⊢z=⟨j,k⟩\to F=C$$
	esum2d.2	$$⊢\phi \to A\in V$$
	esum2d.3	$$⊢\left(\phi \wedge j\in A\right)\to B\in W$$
	esum2d.4	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in B\right)\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
	esum2dlem.e	$$⊢\phi \to A\in \mathrm{Fin}$$
Assertion	esum2dlem	$$⊢\phi \to \underset{j\in A}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$

Proof

Step	Hyp	Ref	Expression
1		esum2d.0	$$⊢\underset{\_}{Ⅎ}kF$$
2		esum2d.1	$$⊢z=⟨j,k⟩\to F=C$$
3		esum2d.2	$$⊢\phi \to A\in V$$
4		esum2d.3	$$⊢\left(\phi \wedge j\in A\right)\to B\in W$$
5		esum2d.4	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in B\right)\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
6		esum2dlem.e	$$⊢\phi \to A\in \mathrm{Fin}$$
7		esumeq1	$$⊢a=\varnothing \to \underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{j\in \varnothing }{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C$$
8		nfv	$$⊢Ⅎza=\varnothing$$
9		iuneq1	$$⊢a=\varnothing \to \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)$$
10	8 9	esumeq1d	$$⊢a=\varnothing \to \underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
11	7 10	eqeq12d	$$⊢a=\varnothing \to \left(\underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\leftrightarrow \underset{j\in \varnothing }{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)$$
12		esumeq1	$$⊢a=b\to \underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C$$
13		nfv	$$⊢Ⅎza=b$$
14		iuneq1	$$⊢a=b\to \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)$$
15	13 14	esumeq1d	$$⊢a=b\to \underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
16	12 15	eqeq12d	$$⊢a=b\to \left(\underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\leftrightarrow \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)$$
17		esumeq1	$$⊢a=b\cup \left\{l\right\}\to \underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{j\in b\cup \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C$$
18		nfv	$$⊢Ⅎza=b\cup \left\{l\right\}$$
19		iuneq1	$$⊢a=b\cup \left\{l\right\}\to \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)$$
20	18 19	esumeq1d	$$⊢a=b\cup \left\{l\right\}\to \underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
21	17 20	eqeq12d	$$⊢a=b\cup \left\{l\right\}\to \left(\underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\leftrightarrow \underset{j\in b\cup \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)$$
22		esumeq1	$$⊢a=A\to \underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{j\in A}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C$$
23		nfv	$$⊢Ⅎza=A$$
24		iuneq1	$$⊢a=A\to \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
25	23 24	esumeq1d	$$⊢a=A\to \underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
26	22 25	eqeq12d	$$⊢a=A\to \left(\underset{j\in a}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in a}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\leftrightarrow \underset{j\in A}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)$$
27		esumnul	$$⊢\underset{z\in \varnothing }{{\sum }^{*}}F=0$$
28		0iun	$$⊢\bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)=\varnothing$$
29		esumeq1	$$⊢\bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)=\varnothing \to \underset{z\in \bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \varnothing }{{\sum }^{*}}F$$
30	28 29	ax-mp	$$⊢\underset{z\in \bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \varnothing }{{\sum }^{*}}F$$
31		esumnul	$$⊢\underset{j\in \varnothing }{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=0$$
32	27 30 31	3eqtr4ri	$$⊢\underset{j\in \varnothing }{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
33	32	a1i	$$⊢\phi \to \underset{j\in \varnothing }{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in \varnothing }\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
34		simpr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)\to \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
35		nfcsb1v	$$⊢\underset{\_}{Ⅎ}j⦋l/j⦌B$$
36		nfcsb1v	$$⊢\underset{\_}{Ⅎ}j⦋l/j⦌C$$
37	35 36	nfesum2	$$⊢\underset{\_}{Ⅎ}j\underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C$$
38		csbeq1a	$$⊢j=l\to B=⦋l/j⦌B$$
39		csbeq1a	$$⊢j=l\to C=⦋l/j⦌C$$
40	38 39	esumeq12d	$$⊢j=l\to \underset{k\in B}{{\sum }^{*}}C=\underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C$$
41	40	adantl	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j=l\right)\to \underset{k\in B}{{\sum }^{*}}C=\underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C$$
42		simprr	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to l\in \left(A\setminus b\right)$$
43	42	eldifad	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to l\in A$$
44	4	adantlr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in A\right)\to B\in W$$
45	44	ralrimiva	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \forall j\in AB\in W$$
46		rspcsbela	$$⊢\left(l\in A\wedge \forall j\in AB\in W\right)\to ⦋l/j⦌B\in W$$
47	43 45 46	syl2anc	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to ⦋l/j⦌B\in W$$
48		simpll	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge k\in ⦋l/j⦌B\right)\to \phi$$
49	43	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge k\in ⦋l/j⦌B\right)\to l\in A$$
50		simpr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge k\in ⦋l/j⦌B\right)\to k\in ⦋l/j⦌B$$
51	5	ex	$$⊢\phi \to \left(\left(j\in A\wedge k\in B\right)\to C\in \left[0,\mathrm{+\infty }\right]\right)$$
52	51	sbcimdv	$$⊢\phi \to \left(\underset{\dot{}}{[}l/j\underset{\dot{}}{]}\left(j\in A\wedge k\in B\right)\to \underset{\dot{}}{[}l/j\underset{\dot{}}{]}C\in \left[0,\mathrm{+\infty }\right]\right)$$
53		sbcan	$$⊢\underset{\dot{}}{[}l/j\underset{\dot{}}{]}\left(j\in A\wedge k\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}l/j\underset{\dot{}}{]}j\in A\wedge \underset{\dot{}}{[}l/j\underset{\dot{}}{]}k\in B\right)$$
54		sbcel1v	$$⊢\underset{\dot{}}{[}l/j\underset{\dot{}}{]}j\in A\leftrightarrow l\in A$$
55		sbcel2	$$⊢\underset{\dot{}}{[}l/j\underset{\dot{}}{]}k\in B\leftrightarrow k\in ⦋l/j⦌B$$
56	54 55	anbi12i	$$⊢\left(\underset{\dot{}}{[}l/j\underset{\dot{}}{]}j\in A\wedge \underset{\dot{}}{[}l/j\underset{\dot{}}{]}k\in B\right)\leftrightarrow \left(l\in A\wedge k\in ⦋l/j⦌B\right)$$
57	53 56	bitri	$$⊢\underset{\dot{}}{[}l/j\underset{\dot{}}{]}\left(j\in A\wedge k\in B\right)\leftrightarrow \left(l\in A\wedge k\in ⦋l/j⦌B\right)$$
58		vex	$$⊢l\in \mathrm{V}$$
59		sbcel1g	$$⊢l\in \mathrm{V}\to \left(\underset{\dot{}}{[}l/j\underset{\dot{}}{]}C\in \left[0,\mathrm{+\infty }\right]\leftrightarrow ⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]\right)$$
60	58 59	ax-mp	$$⊢\underset{\dot{}}{[}l/j\underset{\dot{}}{]}C\in \left[0,\mathrm{+\infty }\right]\leftrightarrow ⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]$$
61	52 57 60	3imtr3g	$$⊢\phi \to \left(\left(l\in A\wedge k\in ⦋l/j⦌B\right)\to ⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]\right)$$
62	61	imp	$$⊢\left(\phi \wedge \left(l\in A\wedge k\in ⦋l/j⦌B\right)\right)\to ⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]$$
63	48 49 50 62	syl12anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge k\in ⦋l/j⦌B\right)\to ⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]$$
64	63	ralrimiva	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \forall k\in ⦋l/j⦌B⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]$$
65		nfcv	$$⊢\underset{\_}{Ⅎ}k⦋l/j⦌B$$
66	65	esumcl	$$⊢\left(⦋l/j⦌B\in W\wedge \forall k\in ⦋l/j⦌B⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]$$
67	47 64 66	syl2anc	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C\in \left[0,\mathrm{+\infty }\right]$$
68	37 41 42 67	esumsnf	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{j\in \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C$$
69		nfv	$$⊢Ⅎk\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)$$
70		nfv	$$⊢Ⅎjz=⟨l,k⟩$$
71	36	nfeq2	$$⊢ℲjF=⦋l/j⦌C$$
72	70 71	nfim	$$⊢Ⅎj\left(z=⟨l,k⟩\to F=⦋l/j⦌C\right)$$
73		opeq1	$$⊢j=l\to ⟨j,k⟩=⟨l,k⟩$$
74	73	eqeq2d	$$⊢j=l\to \left(z=⟨j,k⟩\leftrightarrow z=⟨l,k⟩\right)$$
75	39	eqeq2d	$$⊢j=l\to \left(F=C\leftrightarrow F=⦋l/j⦌C\right)$$
76	74 75	imbi12d	$$⊢j=l\to \left(\left(z=⟨j,k⟩\to F=C\right)\leftrightarrow \left(z=⟨l,k⟩\to F=⦋l/j⦌C\right)\right)$$
77	72 76 2	chvarfv	$$⊢z=⟨l,k⟩\to F=⦋l/j⦌C$$
78		vsnid	$$⊢j\in \left\{j\right\}$$
79	78	a1i	$$⊢\left(\left(\phi \wedge j\in A\right)\wedge k\in B\right)\to j\in \left\{j\right\}$$
80		simpr	$$⊢\left(\left(\phi \wedge j\in A\right)\wedge k\in B\right)\to k\in B$$
81	79 80	opelxpd	$$⊢\left(\left(\phi \wedge j\in A\right)\wedge k\in B\right)\to ⟨j,k⟩\in \left(\left\{j\right\}\times B\right)$$
82		xp2nd	$$⊢z\in \left(\left\{j\right\}\times B\right)\to 2^{nd}\left(z\right)\in B$$
83		xp1st	$$⊢z\in \left(\left\{j\right\}\times B\right)\to 1^{st}\left(z\right)\in \left\{j\right\}$$
84		fvex	$$⊢1^{st}\left(z\right)\in \mathrm{V}$$
85	84	elsn	$$⊢1^{st}\left(z\right)\in \left\{j\right\}\leftrightarrow 1^{st}\left(z\right)=j$$
86	83 85	sylib	$$⊢z\in \left(\left\{j\right\}\times B\right)\to 1^{st}\left(z\right)=j$$
87		eqop	$$⊢z\in \left(\left\{j\right\}\times B\right)\to \left(z=⟨j,k⟩\leftrightarrow \left(1^{st}\left(z\right)=j\wedge 2^{nd}\left(z\right)=k\right)\right)$$
88	86 87	mpbirand	$$⊢z\in \left(\left\{j\right\}\times B\right)\to \left(z=⟨j,k⟩\leftrightarrow 2^{nd}\left(z\right)=k\right)$$
89		eqcom	$$⊢2^{nd}\left(z\right)=k\leftrightarrow k=2^{nd}\left(z\right)$$
90	88 89	bitrdi	$$⊢z\in \left(\left\{j\right\}\times B\right)\to \left(z=⟨j,k⟩\leftrightarrow k=2^{nd}\left(z\right)\right)$$
91	90	ad2antlr	$$⊢\left(\left(\left(\phi \wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\wedge k\in B\right)\to \left(z=⟨j,k⟩\leftrightarrow k=2^{nd}\left(z\right)\right)$$
92	91	ralrimiva	$$⊢\left(\left(\phi \wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\to \forall k\in B\left(z=⟨j,k⟩\leftrightarrow k=2^{nd}\left(z\right)\right)$$
93		reu6i	$$⊢\left(2^{nd}\left(z\right)\in B\wedge \forall k\in B\left(z=⟨j,k⟩\leftrightarrow k=2^{nd}\left(z\right)\right)\right)\to \exists !k\in Bz=⟨j,k⟩$$
94	82 92 93	syl2an2	$$⊢\left(\left(\phi \wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\to \exists !k\in Bz=⟨j,k⟩$$
95	81 94	f1mptrn	$$⊢\left(\phi \wedge j\in A\right)\to \mathrm{Fun}{\left(k\in B⟼⟨j,k⟩\right)}^{-1}$$
96	95	ex	$$⊢\phi \to \left(j\in A\to \mathrm{Fun}{\left(k\in B⟼⟨j,k⟩\right)}^{-1}\right)$$
97	96	sbcimdv	$$⊢\phi \to \left(\underset{\dot{}}{[}l/j\underset{\dot{}}{]}j\in A\to \underset{\dot{}}{[}l/j\underset{\dot{}}{]}\mathrm{Fun}{\left(k\in B⟼⟨j,k⟩\right)}^{-1}\right)$$
98		sbcfung	$$⊢l\in \mathrm{V}\to \left(\underset{\dot{}}{[}l/j\underset{\dot{}}{]}\mathrm{Fun}{\left(k\in B⟼⟨j,k⟩\right)}^{-1}\leftrightarrow \mathrm{Fun}⦋l/j⦌{\left(k\in B⟼⟨j,k⟩\right)}^{-1}\right)$$
99		csbcnv	$$⊢{⦋l/j⦌\left(k\in B⟼⟨j,k⟩\right)}^{-1}=⦋l/j⦌{\left(k\in B⟼⟨j,k⟩\right)}^{-1}$$
100		csbmpt12	$$⊢l\in \mathrm{V}\to ⦋l/j⦌\left(k\in B⟼⟨j,k⟩\right)=\left(k\in ⦋l/j⦌B⟼⦋l/j⦌⟨j,k⟩\right)$$
101		csbopg	$$⊢l\in \mathrm{V}\to ⦋l/j⦌⟨j,k⟩=⟨⦋l/j⦌j,⦋l/j⦌k⟩$$
102		csbvarg	$$⊢l\in \mathrm{V}\to ⦋l/j⦌j=l$$
103		csbconstg	$$⊢l\in \mathrm{V}\to ⦋l/j⦌k=k$$
104	102 103	opeq12d	$$⊢l\in \mathrm{V}\to ⟨⦋l/j⦌j,⦋l/j⦌k⟩=⟨l,k⟩$$
105	101 104	eqtrd	$$⊢l\in \mathrm{V}\to ⦋l/j⦌⟨j,k⟩=⟨l,k⟩$$
106	105	mpteq2dv	$$⊢l\in \mathrm{V}\to \left(k\in ⦋l/j⦌B⟼⦋l/j⦌⟨j,k⟩\right)=\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)$$
107	100 106	eqtrd	$$⊢l\in \mathrm{V}\to ⦋l/j⦌\left(k\in B⟼⟨j,k⟩\right)=\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)$$
108	107	cnveqd	$$⊢l\in \mathrm{V}\to {⦋l/j⦌\left(k\in B⟼⟨j,k⟩\right)}^{-1}={\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}$$
109	99 108	eqtr3id	$$⊢l\in \mathrm{V}\to ⦋l/j⦌{\left(k\in B⟼⟨j,k⟩\right)}^{-1}={\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}$$
110	109	funeqd	$$⊢l\in \mathrm{V}\to \left(\mathrm{Fun}⦋l/j⦌{\left(k\in B⟼⟨j,k⟩\right)}^{-1}\leftrightarrow \mathrm{Fun}{\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}\right)$$
111	98 110	bitrd	$$⊢l\in \mathrm{V}\to \left(\underset{\dot{}}{[}l/j\underset{\dot{}}{]}\mathrm{Fun}{\left(k\in B⟼⟨j,k⟩\right)}^{-1}\leftrightarrow \mathrm{Fun}{\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}\right)$$
112	58 111	ax-mp	$$⊢\underset{\dot{}}{[}l/j\underset{\dot{}}{]}\mathrm{Fun}{\left(k\in B⟼⟨j,k⟩\right)}^{-1}\leftrightarrow \mathrm{Fun}{\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}$$
113	97 54 112	3imtr3g	$$⊢\phi \to \left(l\in A\to \mathrm{Fun}{\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}\right)$$
114	113	imp	$$⊢\left(\phi \wedge l\in A\right)\to \mathrm{Fun}{\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}$$
115	43 114	syldan	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \mathrm{Fun}{\left(k\in ⦋l/j⦌B⟼⟨l,k⟩\right)}^{-1}$$
116		vsnid	$$⊢l\in \left\{l\right\}$$
117	116	a1i	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge k\in ⦋l/j⦌B\right)\to l\in \left\{l\right\}$$
118	117 50	opelxpd	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge k\in ⦋l/j⦌B\right)\to ⟨l,k⟩\in \left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
119	1 69 65 77 47 115 63 118	esumc	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C=\underset{z\in \left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}}{{\sum }^{*}}F$$
120		nfab1	$$⊢\underset{\_}{Ⅎ}t\left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}$$
121		nfcv	$$⊢\underset{\_}{Ⅎ}t\left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
122		opeq1	$$⊢i=l\to ⟨i,k⟩=⟨l,k⟩$$
123	122	eqeq2d	$$⊢i=l\to \left(t=⟨i,k⟩\leftrightarrow t=⟨l,k⟩\right)$$
124	123	rexbidv	$$⊢i=l\to \left(\exists k\in ⦋l/j⦌Bt=⟨i,k⟩\leftrightarrow \exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right)$$
125	58 124	rexsn	$$⊢\exists i\in \left\{l\right\}\exists k\in ⦋l/j⦌Bt=⟨i,k⟩\leftrightarrow \exists k\in ⦋l/j⦌Bt=⟨l,k⟩$$
126		elxp2	$$⊢t\in \left(\left\{l\right\}\times ⦋l/j⦌B\right)\leftrightarrow \exists i\in \left\{l\right\}\exists k\in ⦋l/j⦌Bt=⟨i,k⟩$$
127		abid	$$⊢t\in \left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}\leftrightarrow \exists k\in ⦋l/j⦌Bt=⟨l,k⟩$$
128	125 126 127	3bitr4ri	$$⊢t\in \left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}\leftrightarrow t\in \left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
129	120 121 128	eqri	$$⊢\left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}=\left\{l\right\}\times ⦋l/j⦌B$$
130		esumeq1	$$⊢\left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}=\left\{l\right\}\times ⦋l/j⦌B\to \underset{z\in \left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}}{{\sum }^{*}}F=\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
131	129 130	ax-mp	$$⊢\underset{z\in \left\{t|\exists k\in ⦋l/j⦌Bt=⟨l,k⟩\right\}}{{\sum }^{*}}F=\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
132	119 131	eqtrdi	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{k\in ⦋l/j⦌B}{{\sum }^{*}}⦋l/j⦌C=\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
133	68 132	eqtrd	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{j\in \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
134	133	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)\to \underset{j\in \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
135	34 134	oveq12d	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)\to \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C{+}_{𝑒}\underset{j\in \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F{+}_{𝑒}\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
136		nfv	$$⊢Ⅎj\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)$$
137		nfcv	$$⊢\underset{\_}{Ⅎ}jb$$
138		nfcv	$$⊢\underset{\_}{Ⅎ}j\left\{l\right\}$$
139		vex	$$⊢b\in \mathrm{V}$$
140	139	a1i	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to b\in \mathrm{V}$$
141		vsnex	$$⊢\left\{l\right\}\in \mathrm{V}$$
142	141	a1i	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \left\{l\right\}\in \mathrm{V}$$
143	42	eldifbd	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \neg l\in b$$
144		disjsn	$$⊢b\cap \left\{l\right\}=\varnothing \leftrightarrow \neg l\in b$$
145	143 144	sylibr	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to b\cap \left\{l\right\}=\varnothing$$
146		simpll	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to \phi$$
147		simprl	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to b\subseteq A$$
148	147	sselda	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to j\in A$$
149	5	anassrs	$$⊢\left(\left(\phi \wedge j\in A\right)\wedge k\in B\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
150	149	ralrimiva	$$⊢\left(\phi \wedge j\in A\right)\to \forall k\in BC\in \left[0,\mathrm{+\infty }\right]$$
151		nfcv	$$⊢\underset{\_}{Ⅎ}kB$$
152	151	esumcl	$$⊢\left(B\in W\wedge \forall k\in BC\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in B}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
153	4 150 152	syl2anc	$$⊢\left(\phi \wedge j\in A\right)\to \underset{k\in B}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
154	146 148 153	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to \underset{k\in B}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
155		simpll	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in \left\{l\right\}\right)\to \phi$$
156	43	snssd	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \left\{l\right\}\subseteq A$$
157	156	sselda	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in \left\{l\right\}\right)\to j\in A$$
158	155 157 153	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in \left\{l\right\}\right)\to \underset{k\in B}{{\sum }^{*}}C\in \left[0,\mathrm{+\infty }\right]$$
159	136 137 138 140 142 145 154 158	esumsplit	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{j\in b\cup \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C{+}_{𝑒}\underset{j\in \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C$$
160	159	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)\to \underset{j\in b\cup \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C{+}_{𝑒}\underset{j\in \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C$$
161		iunxun	$$⊢\bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \bigcup _{j\in \left\{l\right\}}\left(\left\{j\right\}\times B\right)$$
162	138 35	nfxp	$$⊢\underset{\_}{Ⅎ}j\left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
163		sneq	$$⊢j=l\to \left\{j\right\}=\left\{l\right\}$$
164	163 38	xpeq12d	$$⊢j=l\to \left\{j\right\}\times B=\left\{l\right\}\times ⦋l/j⦌B$$
165	162 164	iunxsngf	$$⊢l\in \mathrm{V}\to \bigcup _{j\in \left\{l\right\}}\left(\left\{j\right\}\times B\right)=\left\{l\right\}\times ⦋l/j⦌B$$
166	58 165	ax-mp	$$⊢\bigcup _{j\in \left\{l\right\}}\left(\left\{j\right\}\times B\right)=\left\{l\right\}\times ⦋l/j⦌B$$
167	166	uneq2i	$$⊢\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \bigcup _{j\in \left\{l\right\}}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
168	161 167	eqtri	$$⊢\bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
169		esumeq1	$$⊢\bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)=\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \left(\left\{l\right\}\times ⦋l/j⦌B\right)\to \underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \left(\left\{l\right\}\times ⦋l/j⦌B\right)}{{\sum }^{*}}F$$
170	168 169	ax-mp	$$⊢\underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \left(\left\{l\right\}\times ⦋l/j⦌B\right)}{{\sum }^{*}}F$$
171		nfv	$$⊢Ⅎz\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)$$
172		nfcv	$$⊢\underset{\_}{Ⅎ}z\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)$$
173		nfcv	$$⊢\underset{\_}{Ⅎ}z\left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
174		vsnex	$$⊢\left\{j\right\}\in \mathrm{V}$$
175	148 44	syldan	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to B\in W$$
176		xpexg	$$⊢\left(\left\{j\right\}\in \mathrm{V}\wedge B\in W\right)\to \left\{j\right\}\times B\in \mathrm{V}$$
177	174 175 176	sylancr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to \left\{j\right\}\times B\in \mathrm{V}$$
178	177	ralrimiva	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \forall j\in b\left\{j\right\}\times B\in \mathrm{V}$$
179		iunexg	$$⊢\left(b\in \mathrm{V}\wedge \forall j\in b\left\{j\right\}\times B\in \mathrm{V}\right)\to \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\in \mathrm{V}$$
180	139 178 179	sylancr	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\in \mathrm{V}$$
181		xpexg	$$⊢\left(\left\{l\right\}\in \mathrm{V}\wedge ⦋l/j⦌B\in W\right)\to \left\{l\right\}\times ⦋l/j⦌B\in \mathrm{V}$$
182	141 47 181	sylancr	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \left\{l\right\}\times ⦋l/j⦌B\in \mathrm{V}$$
183		simpr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to j\in b$$
184	143	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to \neg l\in b$$
185		nelne2	$$⊢\left(j\in b\wedge \neg l\in b\right)\to j\ne l$$
186	183 184 185	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to j\ne l$$
187		disjsn2	$$⊢j\ne l\to \left\{j\right\}\cap \left\{l\right\}=\varnothing$$
188		xpdisj1	$$⊢\left\{j\right\}\cap \left\{l\right\}=\varnothing \to \left(\left\{j\right\}\times B\right)\cap \left(\left\{l\right\}\times ⦋l/j⦌B\right)=\varnothing$$
189	186 187 188	3syl	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge j\in b\right)\to \left(\left\{j\right\}\times B\right)\cap \left(\left\{l\right\}\times ⦋l/j⦌B\right)=\varnothing$$
190	189	iuneq2dv	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \bigcup _{j\in b}\left(\left(\left\{j\right\}\times B\right)\cap \left(\left\{l\right\}\times ⦋l/j⦌B\right)\right)=\bigcup _{j\in b}\varnothing$$
191	162	iunin1f	$$⊢\bigcup _{j\in b}\left(\left(\left\{j\right\}\times B\right)\cap \left(\left\{l\right\}\times ⦋l/j⦌B\right)\right)=\bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cap \left(\left\{l\right\}\times ⦋l/j⦌B\right)$$
192		iun0	$$⊢\bigcup _{j\in b}\varnothing =\varnothing$$
193	190 191 192	3eqtr3g	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cap \left(\left\{l\right\}\times ⦋l/j⦌B\right)=\varnothing$$
194		simpll	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\right)\to \phi$$
195		iunss1	$$⊢b\subseteq A\to \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\subseteq \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
196	147 195	syl	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\subseteq \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
197	196	sselda	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\right)\to z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
198		nfv	$$⊢Ⅎj\phi$$
199		nfiu1	$$⊢\underset{\_}{Ⅎ}j\bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
200	199	nfcri	$$⊢Ⅎjz\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
201	198 200	nfan	$$⊢Ⅎj\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)$$
202		nfv	$$⊢Ⅎk\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)$$
203		nfcv	$$⊢\underset{\_}{Ⅎ}k\left[0,\mathrm{+\infty }\right]$$
204	1 203	nfel	$$⊢ℲkF\in \left[0,\mathrm{+\infty }\right]$$
205	2	adantl	$$⊢\left(\left(\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\wedge k\in B\right)\wedge z=⟨j,k⟩\right)\to F=C$$
206		simp-5l	$$⊢\left(\left(\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\wedge k\in B\right)\wedge z=⟨j,k⟩\right)\to \phi$$
207		simp-4r	$$⊢\left(\left(\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\wedge k\in B\right)\wedge z=⟨j,k⟩\right)\to j\in A$$
208		simplr	$$⊢\left(\left(\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\wedge k\in B\right)\wedge z=⟨j,k⟩\right)\to k\in B$$
209	206 207 208 5	syl12anc	$$⊢\left(\left(\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\wedge k\in B\right)\wedge z=⟨j,k⟩\right)\to C\in \left[0,\mathrm{+\infty }\right]$$
210	205 209	eqeltrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\wedge k\in B\right)\wedge z=⟨j,k⟩\right)\to F\in \left[0,\mathrm{+\infty }\right]$$
211		elsnxp	$$⊢j\in A\to \left(z\in \left(\left\{j\right\}\times B\right)\leftrightarrow \exists k\in Bz=⟨j,k⟩\right)$$
212	211	biimpa	$$⊢\left(j\in A\wedge z\in \left(\left\{j\right\}\times B\right)\right)\to \exists k\in Bz=⟨j,k⟩$$
213	212	adantll	$$⊢\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\to \exists k\in Bz=⟨j,k⟩$$
214	202 204 210 213	r19.29af2	$$⊢\left(\left(\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\wedge j\in A\right)\wedge z\in \left(\left\{j\right\}\times B\right)\right)\to F\in \left[0,\mathrm{+\infty }\right]$$
215		simpr	$$⊢\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\to z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
216		eliun	$$⊢z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\leftrightarrow \exists j\in Az\in \left(\left\{j\right\}\times B\right)$$
217	215 216	sylib	$$⊢\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\to \exists j\in Az\in \left(\left\{j\right\}\times B\right)$$
218	201 214 217	r19.29af	$$⊢\left(\phi \wedge z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)\right)\to F\in \left[0,\mathrm{+\infty }\right]$$
219	194 197 218	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\right)\to F\in \left[0,\mathrm{+\infty }\right]$$
220		simpll	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge z\in \left(\left\{l\right\}\times ⦋l/j⦌B\right)\right)\to \phi$$
221		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
222		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
223	221 222 162 164	ssiun2sf	$$⊢l\in A\to \left\{l\right\}\times ⦋l/j⦌B\subseteq \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
224	43 223	syl	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \left\{l\right\}\times ⦋l/j⦌B\subseteq \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
225	224	sselda	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge z\in \left(\left\{l\right\}\times ⦋l/j⦌B\right)\right)\to z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)$$
226	220 225 218	syl2anc	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge z\in \left(\left\{l\right\}\times ⦋l/j⦌B\right)\right)\to F\in \left[0,\mathrm{+\infty }\right]$$
227	171 172 173 180 182 193 219 226	esumsplit	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)\cup \left(\left\{l\right\}\times ⦋l/j⦌B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F{+}_{𝑒}\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
228	170 227	eqtrid	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F{+}_{𝑒}\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
229	228	adantr	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)\to \underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F{+}_{𝑒}\underset{z\in \left\{l\right\}\times ⦋l/j⦌B}{{\sum }^{*}}F$$
230	135 160 229	3eqtr4d	$$⊢\left(\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\wedge \underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)\to \underset{j\in b\cup \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$
231	230	ex	$$⊢\left(\phi \wedge \left(b\subseteq A\wedge l\in \left(A\setminus b\right)\right)\right)\to \left(\underset{j\in b}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\to \underset{j\in b\cup \left\{l\right\}}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in b\cup \left\{l\right\}}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F\right)$$
232	11 16 21 26 33 231 6	findcard2d	$$⊢\phi \to \underset{j\in A}{{\sum }^{*}}\underset{k\in B}{{\sum }^{*}}C=\underset{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}{{\sum }^{*}}F$$