Theorem esum2d

Description: Write a double extended sum as a sum over a two-dimensional region. Note that B ( j ) is a function of j . This can be seen as "slicing" the relation A . (Contributed by Thierry Arnoux, 17-May-2020)

	Ref	Expression
Hypotheses	esum2d.0	|- F/_ k F
	esum2d.1	|- ( z = <. j , k >. -> F = C )
	esum2d.2	|- ( ph -> A e. V )
	esum2d.3	|- ( ( ph /\ j e. A ) -> B e. W )
	esum2d.4	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
Assertion	esum2d	|- ( ph -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) F )

Proof

Step	Hyp	Ref	Expression
1		esum2d.0	|- F/_ k F
2		esum2d.1	|- ( z = <. j , k >. -> F = C )
3		esum2d.2	|- ( ph -> A e. V )
4		esum2d.3	|- ( ( ph /\ j e. A ) -> B e. W )
5		esum2d.4	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
6		xrltso	|- < Or RR*
7	6	a1i	|- ( ph -> < Or RR* )
8		nfv	|- F/ c ph
9		nfcv	|- F/_ c s
10		nfmpt1	|- F/_ c ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
11	10	nfrn	|- F/_ c ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
12	9 11	nfel	|- F/ c s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
13	8 12	nfan	|- F/ c ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) )
14		iccssxr	|- ( 0 [,] +oo ) C_ RR*
15		xrge0base	|- ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
16		xrge0cmn	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
17	16	a1i	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
18		simpr	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
19	18	elin2d	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c e. Fin )
20		simpll	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> ph )
21	18	elin1d	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c e. ~P U_ j e. A ( { j } X. B ) )
22	21	adantr	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> c e. ~P U_ j e. A ( { j } X. B ) )
23		vex	|- c e. _V
24	23	elpw	|- ( c e. ~P U_ j e. A ( { j } X. B ) <-> c C_ U_ j e. A ( { j } X. B ) )
25	22 24	sylib	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> c C_ U_ j e. A ( { j } X. B ) )
26		simpr	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> z e. c )
27	25 26	sseldd	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> z e. U_ j e. A ( { j } X. B ) )
28		nfv	|- F/ j ph
29		nfcv	|- F/_ j z
30		nfiu1	|- F/_ j U_ j e. A ( { j } X. B )
31	29 30	nfel	|- F/ j z e. U_ j e. A ( { j } X. B )
32	28 31	nfan	|- F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) )
33		nfv	|- F/ k ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) )
34		nfcv	|- F/_ k ( 0 [,] +oo )
35	1 34	nfel	|- F/ k F e. ( 0 [,] +oo )
36	2	adantl	|- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> F = C )
37		simp-5l	|- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> ph )
38		simp-4r	|- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> j e. A )
39		simplr	|- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> k e. B )
40	37 38 39 5	syl12anc	|- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> C e. ( 0 [,] +oo ) )
41	36 40	eqeltrd	|- ( ( ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. B ) /\ z = <. j , k >. ) -> F e. ( 0 [,] +oo ) )
42		elsnxp	|- ( j e. A -> ( z e. ( { j } X. B ) <-> E. k e. B z = <. j , k >. ) )
43	42	biimpa	|- ( ( j e. A /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
44	43	adantll	|- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. )
45	33 35 41 44	r19.29af2	|- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
46		simpr	|- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> z e. U_ j e. A ( { j } X. B ) )
47		eliun	|- ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) )
48	46 47	sylib	|- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> E. j e. A z e. ( { j } X. B ) )
49	32 45 48	r19.29af	|- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
50	20 27 49	syl2anc	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> F e. ( 0 [,] +oo ) )
51	50	ralrimiva	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> A. z e. c F e. ( 0 [,] +oo ) )
52	15 17 19 51	gsummptcl	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. ( 0 [,] +oo ) )
53	14 52	sselid	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. RR* )
54	53	ralrimiva	|- ( ph -> A. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. RR* )
55		eqid	|- ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) = ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
56	55	rnmptss	|- ( A. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. RR* -> ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) C_ RR* )
57	54 56	syl	|- ( ph -> ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) C_ RR* )
58	57	ad3antrrr	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) C_ RR* )
59		simpllr	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) )
60	58 59	sseldd	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s e. RR* )
61		snex	|- { j } e. _V
62		xpexg	|- ( ( { j } e. _V /\ B e. W ) -> ( { j } X. B ) e. _V )
63	61 4 62	sylancr	|- ( ( ph /\ j e. A ) -> ( { j } X. B ) e. _V )
64	63	ralrimiva	|- ( ph -> A. j e. A ( { j } X. B ) e. _V )
65		iunexg	|- ( ( A e. V /\ A. j e. A ( { j } X. B ) e. _V ) -> U_ j e. A ( { j } X. B ) e. _V )
66	3 64 65	syl2anc	|- ( ph -> U_ j e. A ( { j } X. B ) e. _V )
67	49	ralrimiva	|- ( ph -> A. z e. U_ j e. A ( { j } X. B ) F e. ( 0 [,] +oo ) )
68		nfcv	|- F/_ z U_ j e. A ( { j } X. B )
69	68	esumcl	|- ( ( U_ j e. A ( { j } X. B ) e. _V /\ A. z e. U_ j e. A ( { j } X. B ) F e. ( 0 [,] +oo ) ) -> sum* z e. U_ j e. A ( { j } X. B ) F e. ( 0 [,] +oo ) )
70	66 67 69	syl2anc	|- ( ph -> sum* z e. U_ j e. A ( { j } X. B ) F e. ( 0 [,] +oo ) )
71	14 70	sselid	|- ( ph -> sum* z e. U_ j e. A ( { j } X. B ) F e. RR* )
72	71	ad3antrrr	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> sum* z e. U_ j e. A ( { j } X. B ) F e. RR* )
73		simpr	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
74		nfv	|- F/ z ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
75		nfcv	|- F/_ z c
76	74 75 19 50	esumgsum	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* z e. c F = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
77	66	adantr	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> U_ j e. A ( { j } X. B ) e. _V )
78	49	adantlr	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
79	21 24	sylib	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c C_ U_ j e. A ( { j } X. B ) )
80	74 77 78 79	esummono	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* z e. c F <_ sum* z e. U_ j e. A ( { j } X. B ) F )
81	76 80	eqbrtrrd	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) <_ sum* z e. U_ j e. A ( { j } X. B ) F )
82	81	adantlr	|- ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) <_ sum* z e. U_ j e. A ( { j } X. B ) F )
83	82	adantr	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) <_ sum* z e. U_ j e. A ( { j } X. B ) F )
84	73 83	eqbrtrd	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s <_ sum* z e. U_ j e. A ( { j } X. B ) F )
85		xrlenlt	|- ( ( s e. RR* /\ sum* z e. U_ j e. A ( { j } X. B ) F e. RR* ) -> ( s <_ sum* z e. U_ j e. A ( { j } X. B ) F <-> -. sum* z e. U_ j e. A ( { j } X. B ) F < s ) )
86	85	biimpa	|- ( ( ( s e. RR* /\ sum* z e. U_ j e. A ( { j } X. B ) F e. RR* ) /\ s <_ sum* z e. U_ j e. A ( { j } X. B ) F ) -> -. sum* z e. U_ j e. A ( { j } X. B ) F < s )
87	60 72 84 86	syl21anc	|- ( ( ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> -. sum* z e. U_ j e. A ( { j } X. B ) F < s )
88		simpr	|- ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) -> s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) )
89		ovex	|- ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. _V
90	55 89	elrnmpti	|- ( s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) <-> E. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
91	88 90	sylib	|- ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) -> E. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
92	13 87 91	r19.29af	|- ( ( ph /\ s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) -> -. sum* z e. U_ j e. A ( { j } X. B ) F < s )
93	92	ralrimiva	|- ( ph -> A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. sum* z e. U_ j e. A ( { j } X. B ) F < s )
94		nfv	|- F/ c ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F )
95		nfv	|- F/ c s < t
96	11 95	nfrex	|- F/ c E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t
97	76	adantlr	|- ( ( ( ph /\ s e. RR* ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* z e. c F = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
98	97	adantlr	|- ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* z e. c F = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
99	98	adantr	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) -> sum* z e. c F = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
100		simplr	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) -> c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
101	89	a1i	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. _V )
102	55	elrnmpt1	|- ( ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. _V ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) )
103	100 101 102	syl2anc	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) )
104	99 103	eqeltrd	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) -> sum* z e. c F e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) )
105		simpr	|- ( ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) /\ t = sum* z e. c F ) -> t = sum* z e. c F )
106	105	breq2d	|- ( ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) /\ t = sum* z e. c F ) -> ( s < t <-> s < sum* z e. c F ) )
107		simpr	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) -> s < sum* z e. c F )
108	104 106 107	rspcedvd	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ s < sum* z e. c F ) -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t )
109		nfv	|- F/ z ( ph /\ s e. RR* )
110		nfcv	|- F/_ z s
111		nfcv	|- F/_ z <
112	68	nfesum1	|- F/_ z sum* z e. U_ j e. A ( { j } X. B ) F
113	110 111 112	nfbr	|- F/ z s < sum* z e. U_ j e. A ( { j } X. B ) F
114	109 113	nfan	|- F/ z ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F )
115	66	ad2antrr	|- ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) -> U_ j e. A ( { j } X. B ) e. _V )
116	49	3ad2antr3	|- ( ( ph /\ ( s e. RR* /\ s < sum* z e. U_ j e. A ( { j } X. B ) F /\ z e. U_ j e. A ( { j } X. B ) ) ) -> F e. ( 0 [,] +oo ) )
117	116	3anassrs	|- ( ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
118		simplr	|- ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) -> s e. RR* )
119		simpr	|- ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) -> s < sum* z e. U_ j e. A ( { j } X. B ) F )
120	114 115 117 118 119	esumlub	|- ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) -> E. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) s < sum* z e. c F )
121	94 96 108 120	r19.29af2	|- ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t )
122	121	ex	|- ( ( ph /\ s e. RR* ) -> ( s < sum* z e. U_ j e. A ( { j } X. B ) F -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) )
123	122	ralrimiva	|- ( ph -> A. s e. RR* ( s < sum* z e. U_ j e. A ( { j } X. B ) F -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) )
124	93 123	jca	|- ( ph -> ( A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. sum* z e. U_ j e. A ( { j } X. B ) F < s /\ A. s e. RR* ( s < sum* z e. U_ j e. A ( { j } X. B ) F -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) )
125		simpr	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> r = sum* z e. U_ j e. A ( { j } X. B ) F )
126	125	breq1d	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> ( r < s <-> sum* z e. U_ j e. A ( { j } X. B ) F < s ) )
127	126	notbid	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> ( -. r < s <-> -. sum* z e. U_ j e. A ( { j } X. B ) F < s ) )
128	127	ralbidv	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> ( A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. r < s <-> A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. sum* z e. U_ j e. A ( { j } X. B ) F < s ) )
129	125	breq2d	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> ( s < r <-> s < sum* z e. U_ j e. A ( { j } X. B ) F ) )
130	129	imbi1d	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> ( ( s < r -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) <-> ( s < sum* z e. U_ j e. A ( { j } X. B ) F -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) )
131	130	ralbidv	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> ( A. s e. RR* ( s < r -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) <-> A. s e. RR* ( s < sum* z e. U_ j e. A ( { j } X. B ) F -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) )
132	128 131	anbi12d	|- ( ( ph /\ r = sum* z e. U_ j e. A ( { j } X. B ) F ) -> ( ( A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. r < s /\ A. s e. RR* ( s < r -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) <-> ( A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. sum* z e. U_ j e. A ( { j } X. B ) F < s /\ A. s e. RR* ( s < sum* z e. U_ j e. A ( { j } X. B ) F -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) ) )
133	71 132	rspcedv	|- ( ph -> ( ( A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. sum* z e. U_ j e. A ( { j } X. B ) F < s /\ A. s e. RR* ( s < sum* z e. U_ j e. A ( { j } X. B ) F -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) -> E. r e. RR* ( A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. r < s /\ A. s e. RR* ( s < r -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) ) )
134	124 133	mpd	|- ( ph -> E. r e. RR* ( A. s e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -. r < s /\ A. s e. RR* ( s < r -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) ) )
135	7 134	supcl	|- ( ph -> sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) e. RR* )
136		nfv	|- F/ a ph
137		nfcv	|- F/_ a s
138		nfmpt1	|- F/_ a ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
139	138	nfrn	|- F/_ a ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
140	137 139	nfel	|- F/ a s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
141	136 140	nfan	|- F/ a ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
142		simpr	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. ( ~P A i^i Fin ) )
143		simpll	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> ph )
144	142	elin1d	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. ~P A )
145		elpwi	|- ( a e. ~P A -> a C_ A )
146	144 145	syl	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a C_ A )
147	146	sselda	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> j e. A )
148	143 147 4	syl2anc	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> B e. W )
149	143	adantrr	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> ph )
150	147	adantrr	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> j e. A )
151		simprr	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> k e. B )
152	149 150 151 5	syl12anc	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
153	142	elin2d	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. Fin )
154	1 2 142 148 152 153	esum2dlem	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> sum* j e. a sum* k e. B C = sum* z e. U_ j e. a ( { j } X. B ) F )
155		nfv	|- F/ j ( ph /\ a e. ( ~P A i^i Fin ) )
156		nfcv	|- F/_ j a
157	5	anassrs	|- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
158	157	ralrimiva	|- ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
159		nfcv	|- F/_ k B
160	159	esumcl	|- ( ( B e. W /\ A. k e. B C e. ( 0 [,] +oo ) ) -> sum* k e. B C e. ( 0 [,] +oo ) )
161	4 158 160	syl2anc	|- ( ( ph /\ j e. A ) -> sum* k e. B C e. ( 0 [,] +oo ) )
162	143 147 161	syl2anc	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> sum* k e. B C e. ( 0 [,] +oo ) )
163	155 156 153 162	esumgsum	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> sum* j e. a sum* k e. B C = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
164	154 163	eqtr3d	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> sum* z e. U_ j e. a ( { j } X. B ) F = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
165		nfv	|- F/ z ( ph /\ a e. ( ~P A i^i Fin ) )
166	66	adantr	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> U_ j e. A ( { j } X. B ) e. _V )
167	49	adantlr	|- ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
168		iunss1	|- ( a C_ A -> U_ j e. a ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
169	146 168	syl	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> U_ j e. a ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
170	165 166 167 169	esummono	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> sum* z e. U_ j e. a ( { j } X. B ) F <_ sum* z e. U_ j e. A ( { j } X. B ) F )
171	164 170	eqbrtrrd	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) <_ sum* z e. U_ j e. A ( { j } X. B ) F )
172	16	a1i	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
173	162	ralrimiva	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> A. j e. a sum* k e. B C e. ( 0 [,] +oo ) )
174	15 172 153 173	gsummptcl	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) e. ( 0 [,] +oo ) )
175	14 174	sselid	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) e. RR* )
176	71	adantr	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> sum* z e. U_ j e. A ( { j } X. B ) F e. RR* )
177		xrlenlt	|- ( ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) e. RR* /\ sum* z e. U_ j e. A ( { j } X. B ) F e. RR* ) -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) <_ sum* z e. U_ j e. A ( { j } X. B ) F <-> -. sum* z e. U_ j e. A ( { j } X. B ) F < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
178	175 176 177	syl2anc	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) <_ sum* z e. U_ j e. A ( { j } X. B ) F <-> -. sum* z e. U_ j e. A ( { j } X. B ) F < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
179	171 178	mpbid	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> -. sum* z e. U_ j e. A ( { j } X. B ) F < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
180		nfv	|- F/ z ph
181		eqidd	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
182	180 68 66 49 181	esumval	|- ( ph -> sum* z e. U_ j e. A ( { j } X. B ) F = sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) )
183	182	adantr	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> sum* z e. U_ j e. A ( { j } X. B ) F = sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) )
184	183	breq1d	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( sum* z e. U_ j e. A ( { j } X. B ) F < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) <-> sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
185	179 184	mtbid	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> -. sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
186	185	adantlr	|- ( ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) -> -. sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
187	186	adantr	|- ( ( ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) -> -. sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
188		simpr	|- ( ( ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) -> s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
189	188	breq2d	|- ( ( ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) -> ( sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < s <-> sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
190	189	notbid	|- ( ( ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) -> ( -. sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < s <-> -. sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
191	187 190	mpbird	|- ( ( ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) /\ a e. ( ~P A i^i Fin ) ) /\ s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) -> -. sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < s )
192		eqid	|- ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) = ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
193		ovex	|- ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) e. _V
194	192 193	elrnmpti	|- ( s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) <-> E. a e. ( ~P A i^i Fin ) s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
195	194	biimpi	|- ( s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) -> E. a e. ( ~P A i^i Fin ) s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
196	195	adantl	|- ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) -> E. a e. ( ~P A i^i Fin ) s = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
197	141 191 196	r19.29af	|- ( ( ph /\ s e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) ) -> -. sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) < s )
198	9	nfel1	|- F/ c s e. RR*
199		nfcv	|- F/_ c <
200		nfcv	|- F/_ c RR*
201	11 200 199	nfsup	|- F/_ c sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < )
202	9 199 201	nfbr	|- F/ c s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < )
203	198 202	nfan	|- F/ c ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) )
204	8 203	nfan	|- F/ c ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) )
205		nfcv	|- F/_ c u
206	205 11	nfel	|- F/ c u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
207	204 206	nfan	|- F/ c ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) )
208		nfv	|- F/ c s < u
209	207 208	nfan	|- F/ c ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u )
210		simp-5l	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> ph )
211		simpr1l	|- ( ( ph /\ ( ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ ( s < u /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) ) -> s e. RR* )
212	211	3anassrs	|- ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ ( s < u /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) -> s e. RR* )
213	212	3anassrs	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s e. RR* )
214	210 213	jca	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> ( ph /\ s e. RR* ) )
215		simpr1r	|- ( ( ph /\ ( ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ ( s < u /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) ) -> s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) )
216	215	3anassrs	|- ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ ( s < u /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) -> s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) )
217	216	3anassrs	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) )
218	214 217	jca	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> ( ( ph /\ s e. RR* ) /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) )
219		simpllr	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s < u )
220		simpr	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
221	219 220	breqtrd	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
222		simplr	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
223		simpr	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
224	223	elin1d	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c e. ~P U_ j e. A ( { j } X. B ) )
225		elpwi	|- ( c e. ~P U_ j e. A ( { j } X. B ) -> c C_ U_ j e. A ( { j } X. B ) )
226		dmss	|- ( c C_ U_ j e. A ( { j } X. B ) -> dom c C_ dom U_ j e. A ( { j } X. B ) )
227		dmiun	|- dom U_ j e. A ( { j } X. B ) = U_ j e. A dom ( { j } X. B )
228	226 227	sseqtrdi	|- ( c C_ U_ j e. A ( { j } X. B ) -> dom c C_ U_ j e. A dom ( { j } X. B ) )
229		dmxpss	|- dom ( { j } X. B ) C_ { j }
230	229	a1i	|- ( j e. A -> dom ( { j } X. B ) C_ { j } )
231		snssi	|- ( j e. A -> { j } C_ A )
232	230 231	sstrd	|- ( j e. A -> dom ( { j } X. B ) C_ A )
233	232	rgen	|- A. j e. A dom ( { j } X. B ) C_ A
234		iunss	|- ( U_ j e. A dom ( { j } X. B ) C_ A <-> A. j e. A dom ( { j } X. B ) C_ A )
235	233 234	mpbir	|- U_ j e. A dom ( { j } X. B ) C_ A
236	228 235	sstrdi	|- ( c C_ U_ j e. A ( { j } X. B ) -> dom c C_ A )
237	23	dmex	|- dom c e. _V
238	237	elpw	|- ( dom c e. ~P A <-> dom c C_ A )
239	236 238	sylibr	|- ( c C_ U_ j e. A ( { j } X. B ) -> dom c e. ~P A )
240	224 225 239	3syl	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c e. ~P A )
241	223	elin2d	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c e. Fin )
242		dmfi	|- ( c e. Fin -> dom c e. Fin )
243	241 242	syl	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c e. Fin )
244	240 243	elind	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c e. ( ~P A i^i Fin ) )
245		ovex	|- ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. _V
246	245	a1i	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. _V )
247		mpteq1	|- ( a = dom c -> ( j e. a |-> sum* k e. B C ) = ( j e. dom c |-> sum* k e. B C ) )
248	247	oveq2d	|- ( a = dom c -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
249	192 248	elrnmpt1s	|- ( ( dom c e. ( ~P A i^i Fin ) /\ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. _V ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
250	244 246 249	syl2anc	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) )
251		simpr	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ t = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) ) -> t = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
252	251	breq2d	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ t = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) ) -> ( s < t <-> s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) ) )
253		simpllr	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> s e. RR* )
254	16	a1i	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
255		nfcv	|- F/_ z ( RR*s |`s ( 0 [,] +oo ) )
256		nfcv	|- F/_ z gsum
257		nfmpt1	|- F/_ z ( z e. c |-> F )
258	255 256 257	nfov	|- F/_ z ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) )
259	110 111 258	nfbr	|- F/ z s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) )
260	109 259	nfan	|- F/ z ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
261		nfv	|- F/ z c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin )
262	260 261	nfan	|- F/ z ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
263		simp-4l	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> ph )
264	224 225	syl	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c C_ U_ j e. A ( { j } X. B ) )
265	264	sselda	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> z e. U_ j e. A ( { j } X. B ) )
266	263 265 49	syl2anc	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> F e. ( 0 [,] +oo ) )
267	266	ex	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( z e. c -> F e. ( 0 [,] +oo ) ) )
268	262 267	ralrimi	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> A. z e. c F e. ( 0 [,] +oo ) )
269	15 254 241 268	gsummptcl	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. ( 0 [,] +oo ) )
270	14 269	sselid	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. RR* )
271		nfv	|- F/ j ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
272		nfcv	|- F/_ j c
273	30	nfpw	|- F/_ j ~P U_ j e. A ( { j } X. B )
274		nfcv	|- F/_ j Fin
275	273 274	nfin	|- F/_ j ( ~P U_ j e. A ( { j } X. B ) i^i Fin )
276	272 275	nfel	|- F/ j c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin )
277	271 276	nfan	|- F/ j ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
278		simpll	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ph )
279	79 236	syl	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c C_ A )
280	279	sselda	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> j e. A )
281	278 280 161	syl2anc	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> sum* k e. B C e. ( 0 [,] +oo ) )
282	281	adantllr	|- ( ( ( ( ph /\ s e. RR* ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> sum* k e. B C e. ( 0 [,] +oo ) )
283	282	adantllr	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> sum* k e. B C e. ( 0 [,] +oo ) )
284	283	ex	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( j e. dom c -> sum* k e. B C e. ( 0 [,] +oo ) ) )
285	277 284	ralrimi	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> A. j e. dom c sum* k e. B C e. ( 0 [,] +oo ) )
286	15 254 243 285	gsummptcl	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. ( 0 [,] +oo ) )
287	14 286	sselid	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. RR* )
288		simplr	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
289	28 276	nfan	|- F/ j ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
290		id	|- ( c C_ U_ j e. A ( { j } X. B ) -> c C_ U_ j e. A ( { j } X. B ) )
291		xpss	|- ( { j } X. B ) C_ ( _V X. _V )
292	291	rgenw	|- A. j e. A ( { j } X. B ) C_ ( _V X. _V )
293		iunss	|- ( U_ j e. A ( { j } X. B ) C_ ( _V X. _V ) <-> A. j e. A ( { j } X. B ) C_ ( _V X. _V ) )
294	292 293	mpbir	|- U_ j e. A ( { j } X. B ) C_ ( _V X. _V )
295	294	a1i	|- ( c C_ U_ j e. A ( { j } X. B ) -> U_ j e. A ( { j } X. B ) C_ ( _V X. _V ) )
296	290 295	sstrd	|- ( c C_ U_ j e. A ( { j } X. B ) -> c C_ ( _V X. _V ) )
297	79 296	syl	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c C_ ( _V X. _V ) )
298		df-rel	|- ( Rel c <-> c C_ ( _V X. _V ) )
299	297 298	sylibr	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> Rel c )
300	1 289 15 2 299 19 17 50	gsummpt2d	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( c " { j } ) |-> C ) ) ) ) )
301		nfcv	|- F/_ j dom c
302	237	a1i	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c e. _V )
303	278	adantr	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. ( c " { j } ) ) -> ph )
304	280	adantr	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. ( c " { j } ) ) -> j e. A )
305	79	adantr	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> c C_ U_ j e. A ( { j } X. B ) )
306		imass1	|- ( c C_ U_ j e. A ( { j } X. B ) -> ( c " { j } ) C_ ( U_ j e. A ( { j } X. B ) " { j } ) )
307	305 306	syl	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ( c " { j } ) C_ ( U_ j e. A ( { j } X. B ) " { j } ) )
308	3 4	iunsnima	|- ( ( ph /\ j e. A ) -> ( U_ j e. A ( { j } X. B ) " { j } ) = B )
309	278 280 308	syl2anc	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ( U_ j e. A ( { j } X. B ) " { j } ) = B )
310	307 309	sseqtrd	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ( c " { j } ) C_ B )
311	310	sselda	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. ( c " { j } ) ) -> k e. B )
312	303 304 311 5	syl12anc	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. ( c " { j } ) ) -> C e. ( 0 [,] +oo ) )
313	312	ralrimiva	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> A. k e. ( c " { j } ) C e. ( 0 [,] +oo ) )
314		imaexg	|- ( c e. _V -> ( c " { j } ) e. _V )
315	23 314	ax-mp	|- ( c " { j } ) e. _V
316		nfcv	|- F/_ k ( c " { j } )
317	316	esumcl	|- ( ( ( c " { j } ) e. _V /\ A. k e. ( c " { j } ) C e. ( 0 [,] +oo ) ) -> sum* k e. ( c " { j } ) C e. ( 0 [,] +oo ) )
318	315 317	mpan	|- ( A. k e. ( c " { j } ) C e. ( 0 [,] +oo ) -> sum* k e. ( c " { j } ) C e. ( 0 [,] +oo ) )
319	313 318	syl	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> sum* k e. ( c " { j } ) C e. ( 0 [,] +oo ) )
320		nfv	|- F/ k ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c )
321	278 280 4	syl2anc	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> B e. W )
322	278	adantr	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. B ) -> ph )
323	280	adantr	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. B ) -> j e. A )
324		simpr	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. B ) -> k e. B )
325	322 323 324 5	syl12anc	|- ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
326	320 321 325 310	esummono	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> sum* k e. ( c " { j } ) C <_ sum* k e. B C )
327	289 301 302 319 281 326	esumlef	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* j e. dom c sum* k e. ( c " { j } ) C <_ sum* j e. dom c sum* k e. B C )
328	19 242	syl	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c e. Fin )
329	289 301 328 319	esumgsum	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* j e. dom c sum* k e. ( c " { j } ) C = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. ( c " { j } ) C ) ) )
330	19	adantr	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> c e. Fin )
331		imafi2	|- ( c e. Fin -> ( c " { j } ) e. Fin )
332	330 331	syl	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ( c " { j } ) e. Fin )
333	320 316 332 312	esumgsum	|- ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> sum* k e. ( c " { j } ) C = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( c " { j } ) |-> C ) ) )
334	289 333	mpteq2da	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( j e. dom c |-> sum* k e. ( c " { j } ) C ) = ( j e. dom c |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( c " { j } ) |-> C ) ) ) )
335	334	oveq2d	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. ( c " { j } ) C ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( c " { j } ) |-> C ) ) ) ) )
336	329 335	eqtrd	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* j e. dom c sum* k e. ( c " { j } ) C = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( c " { j } ) |-> C ) ) ) ) )
337	289 301 328 281	esumgsum	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> sum* j e. dom c sum* k e. B C = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
338	327 336 337	3brtr3d	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. ( c " { j } ) |-> C ) ) ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
339	300 338	eqbrtrd	|- ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
340	339	adantlr	|- ( ( ( ph /\ s e. RR* ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
341	340	adantlr	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) <_ ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
342	253 270 287 288 341	xrltletrd	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) )
343	250 252 342	rspcedvd	|- ( ( ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> E. t e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) s < t )
344	343	adantllr	|- ( ( ( ( ( ph /\ s e. RR* ) /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> E. t e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) s < t )
345	218 221 222 344	syl21anc	|- ( ( ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> E. t e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) s < t )
346	55 89	elrnmpti	|- ( u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) <-> E. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
347	346	biimpi	|- ( u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) -> E. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
348	347	ad2antlr	|- ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) -> E. c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) u = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
349	209 345 348	r19.29af	|- ( ( ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) /\ u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) ) /\ s < u ) -> E. t e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) s < t )
350	7 134	suplub	|- ( ph -> ( ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t ) )
351	350	imp	|- ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) -> E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t )
352		breq2	|- ( t = u -> ( s < t <-> s < u ) )
353	352	cbvrexvw	|- ( E. t e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < t <-> E. u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < u )
354	351 353	sylib	|- ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) -> E. u e. ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) s < u )
355	349 354	r19.29a	|- ( ( ph /\ ( s e. RR* /\ s < sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) ) ) -> E. t e. ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) s < t )
356	7 135 197 355	eqsupd	|- ( ph -> sup ( ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) , RR* , < ) = sup ( ran ( c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) ) , RR* , < ) )
357		nfcv	|- F/_ j A
358		eqidd	|- ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
359	28 357 3 161 358	esumval	|- ( ph -> sum* j e. A sum* k e. B C = sup ( ran ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) ) , RR* , < ) )
360	356 359 182	3eqtr4d	|- ( ph -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) F )