Metamath Proof Explorer

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 eliun 
 |-  ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) )
47 46 bilani 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> E. j e. A z e. ( { j } X. B ) )
48 32 45 47 r19.29af 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
49 20 27 48 syl2anc 
 |-  ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ z e. c ) -> F e. ( 0 [,] +oo ) )
50 49 ralrimiva 
 |-  ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> A. z e. c F e. ( 0 [,] +oo ) )
51 15 17 19 50 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 ) )
52 14 51 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* )
53 52 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* )
54 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 ) ) )
55 54 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* )
56 53 55 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* )
57 56 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* )
58 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 ) ) ) )
59 57 58 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* )
60 vsnex 
 |-  { j } e. _V
61 xpexg 
 |-  ( ( { j } e. _V /\ B e. W ) -> ( { j } X. B ) e. _V )
62 60 4 61 sylancr 
 |-  ( ( ph /\ j e. A ) -> ( { j } X. B ) e. _V )
63 62 ralrimiva 
 |-  ( ph -> A. j e. A ( { j } X. B ) e. _V )
64 iunexg 
 |-  ( ( A e. V /\ A. j e. A ( { j } X. B ) e. _V ) -> U_ j e. A ( { j } X. B ) e. _V )
65 3 63 64 syl2anc 
 |-  ( ph -> U_ j e. A ( { j } X. B ) e. _V )
66 48 ralrimiva 
 |-  ( ph -> A. z e. U_ j e. A ( { j } X. B ) F e. ( 0 [,] +oo ) )
67 nfcv 
 |-  F/_ z U_ j e. A ( { j } X. B )
68 67 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 ) )
69 65 66 68 syl2anc 
 |-  ( ph -> sum* z e. U_ j e. A ( { j } X. B ) F e. ( 0 [,] +oo ) )
70 14 69 sselid 
 |-  ( ph -> sum* z e. U_ j e. A ( { j } X. B ) F e. RR* )
71 70 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* )
72 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 ) ) )
73 nfv 
 |-  F/ z ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
74 nfcv 
 |-  F/_ z c
75 73 74 19 49 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 ) ) )
76 65 adantr 
 |-  ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> U_ j e. A ( { j } X. B ) e. _V )
77 48 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 ) )
78 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 ) )
79 73 76 77 78 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 )
80 75 79 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 )
81 80 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 )
82 81 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 )
83 72 82 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 )
84 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 ) )
85 84 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 )
86 59 71 83 85 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 )
87 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) e. _V
88 54 87 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 ) ) )
89 88 bilani 
 |-  ( ( 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 ) ) )
90 13 86 89 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 )
91 90 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 )
92 nfv 
 |-  F/ c ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F )
93 nfv 
 |-  F/ c s < t
94 11 93 nfrexw 
 |-  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
95 75 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 ) ) )
96 95 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 ) ) )
97 96 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 ) ) )
98 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 ) )
99 87 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 )
100 54 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 ) ) ) )
101 98 99 100 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 ) ) ) )
102 97 101 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 ) ) ) )
103 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 )
104 103 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 ) )
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 ) -> s < sum* z e. c F )
106 102 104 105 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 )
107 nfv 
 |-  F/ z ( ph /\ s e. RR* )
108 nfcv 
 |-  F/_ z s
109 nfcv 
 |-  F/_ z <
110 67 nfesum1 
 |-  F/_ z sum* z e. U_ j e. A ( { j } X. B ) F
111 108 109 110 nfbr 
 |-  F/ z s < sum* z e. U_ j e. A ( { j } X. B ) F
112 107 111 nfan 
 |-  F/ z ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F )
113 65 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 )
114 48 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 ) )
115 114 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 ) )
116 simplr 
 |-  ( ( ( ph /\ s e. RR* ) /\ s < sum* z e. U_ j e. A ( { j } X. B ) F ) -> s e. RR* )
117 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 )
118 112 113 115 116 117 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 )
119 92 94 106 118 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 )
120 119 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 ) )
121 120 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 ) )
122 91 121 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 ) ) )
123 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 )
124 123 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 ) )
125 124 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 ) )
126 125 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 ) )
127 123 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 ) )
128 127 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 ) ) )
129 128 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 ) ) )
130 126 129 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 ) ) ) )
131 70 130 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 ) ) ) )
132 122 131 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 ) ) )
133 7 132 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* )
134 nfv 
 |-  F/ a ph
135 nfcv 
 |-  F/_ a s
136 nfmpt1 
 |-  F/_ a ( a e. ( ~P A i^i Fin ) |-> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) )
137 136 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 ) ) )
138 135 137 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 ) ) )
139 134 138 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 ) ) ) )
140 simpr 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. ( ~P A i^i Fin ) )
141 simpll 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> ph )
142 140 elin1d 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. ~P A )
143 elpwi 
 |-  ( a e. ~P A -> a C_ A )
144 142 143 syl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a C_ A )
145 144 sselda 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> j e. A )
146 141 145 4 syl2anc 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> B e. W )
147 141 adantrr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> ph )
148 145 adantrr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> j e. A )
149 simprr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> k e. B )
150 147 148 149 5 syl12anc 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ ( j e. a /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
151 140 elin2d 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> a e. Fin )
152 1 2 140 146 150 151 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 )
153 nfv 
 |-  F/ j ( ph /\ a e. ( ~P A i^i Fin ) )
154 nfcv 
 |-  F/_ j a
155 5 anassrs 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
156 155 ralrimiva 
 |-  ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
157 nfcv 
 |-  F/_ k B
158 157 esumcl 
 |-  ( ( B e. W /\ A. k e. B C e. ( 0 [,] +oo ) ) -> sum* k e. B C e. ( 0 [,] +oo ) )
159 4 156 158 syl2anc 
 |-  ( ( ph /\ j e. A ) -> sum* k e. B C e. ( 0 [,] +oo ) )
160 141 145 159 syl2anc 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ j e. a ) -> sum* k e. B C e. ( 0 [,] +oo ) )
161 153 154 151 160 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 ) ) )
162 152 161 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 ) ) )
163 nfv 
 |-  F/ z ( ph /\ a e. ( ~P A i^i Fin ) )
164 65 adantr 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> U_ j e. A ( { j } X. B ) e. _V )
165 48 adantlr 
 |-  ( ( ( ph /\ a e. ( ~P A i^i Fin ) ) /\ z e. U_ j e. A ( { j } X. B ) ) -> F e. ( 0 [,] +oo ) )
166 iunss1 
 |-  ( a C_ A -> U_ j e. a ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
167 144 166 syl 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> U_ j e. a ( { j } X. B ) C_ U_ j e. A ( { j } X. B ) )
168 163 164 165 167 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 )
169 162 168 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 )
170 16 a1i 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
171 160 ralrimiva 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> A. j e. a sum* k e. B C e. ( 0 [,] +oo ) )
172 15 170 151 171 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 ) )
173 14 172 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* )
174 70 adantr 
 |-  ( ( ph /\ a e. ( ~P A i^i Fin ) ) -> sum* z e. U_ j e. A ( { j } X. B ) F e. RR* )
175 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 ) ) ) )
176 173 174 175 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 ) ) ) )
177 169 176 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 ) ) )
178 nfv 
 |-  F/ z ph
179 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 ) ) )
180 178 67 65 48 179 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* , < ) )
181 180 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* , < ) )
182 181 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 ) ) ) )
183 177 182 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 ) ) )
184 183 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 ) ) )
185 184 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 ) ) )
186 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 ) ) )
187 186 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 ) ) ) )
188 187 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 ) ) ) )
189 185 188 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 )
190 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 ) ) )
191 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. a |-> sum* k e. B C ) ) e. _V
192 190 191 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 ) ) )
193 192 bilani 
 |-  ( ( 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 ) ) )
194 139 189 193 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 )
195 9 nfel1 
 |-  F/ c s e. RR*
196 nfcv 
 |-  F/_ c <
197 nfcv 
 |-  F/_ c RR*
198 11 197 196 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* , < )
199 9 196 198 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* , < )
200 195 199 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* , < ) )
201 8 200 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* , < ) ) )
202 nfcv 
 |-  F/_ c u
203 202 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 ) ) )
204 201 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* , < ) ) ) /\ 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 ) ) ) )
205 nfv 
 |-  F/ c s < u
206 204 205 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 )
207 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 )
208 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* )
209 208 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* )
210 209 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* )
211 207 210 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* ) )
212 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* , < ) )
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 < 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* , < ) )
214 213 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* , < ) )
215 211 214 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* , < ) ) )
216 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 )
217 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 ) ) )
218 216 217 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 ) ) )
219 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 ) )
220 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 ) )
221 220 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 ) )
222 elpwi 
 |-  ( c e. ~P U_ j e. A ( { j } X. B ) -> c C_ U_ j e. A ( { j } X. B ) )
223 dmss 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> dom c C_ dom U_ j e. A ( { j } X. B ) )
224 dmiun 
 |-  dom U_ j e. A ( { j } X. B ) = U_ j e. A dom ( { j } X. B )
225 223 224 sseqtrdi 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> dom c C_ U_ j e. A dom ( { j } X. B ) )
226 dmxpss 
 |-  dom ( { j } X. B ) C_ { j }
227 226 a1i 
 |-  ( j e. A -> dom ( { j } X. B ) C_ { j } )
228 snssi 
 |-  ( j e. A -> { j } C_ A )
229 227 228 sstrd 
 |-  ( j e. A -> dom ( { j } X. B ) C_ A )
230 229 rgen 
 |-  A. j e. A dom ( { j } X. B ) C_ A
231 iunss 
 |-  ( U_ j e. A dom ( { j } X. B ) C_ A <-> A. j e. A dom ( { j } X. B ) C_ A )
232 230 231 mpbir 
 |-  U_ j e. A dom ( { j } X. B ) C_ A
233 225 232 sstrdi 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> dom c C_ A )
234 23 dmex 
 |-  dom c e. _V
235 234 elpw 
 |-  ( dom c e. ~P A <-> dom c C_ A )
236 233 235 sylibr 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> dom c e. ~P A )
237 221 222 236 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 )
238 220 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 )
239 dmfi 
 |-  ( c e. Fin -> dom c e. Fin )
240 238 239 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 )
241 237 240 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 ) )
242 ovex 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( j e. dom c |-> sum* k e. B C ) ) e. _V
243 242 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 )
244 mpteq1 
 |-  ( a = dom c -> ( j e. a |-> sum* k e. B C ) = ( j e. dom c |-> sum* k e. B C ) )
245 244 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 ) ) )
246 190 245 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 ) ) ) )
247 241 243 246 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 ) ) ) )
248 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 ) ) )
249 248 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 ) ) ) )
250 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* )
251 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 )
252 nfcv 
 |-  F/_ z ( RR*s |`s ( 0 [,] +oo ) )
253 nfcv 
 |-  F/_ z gsum
254 nfmpt1 
 |-  F/_ z ( z e. c |-> F )
255 252 253 254 nfov 
 |-  F/_ z ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) )
256 108 109 255 nfbr 
 |-  F/ z s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) )
257 107 256 nfan 
 |-  F/ z ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
258 nfv 
 |-  F/ z c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin )
259 257 258 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 ) )
260 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 )
261 221 222 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 ) )
262 261 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 ) )
263 260 262 48 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 ) )
264 263 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 ) ) )
265 259 264 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 ) )
266 15 251 238 265 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 ) )
267 14 266 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* )
268 nfv 
 |-  F/ j ( ( ph /\ s e. RR* ) /\ s < ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( z e. c |-> F ) ) )
269 nfcv 
 |-  F/_ j c
270 30 nfpw 
 |-  F/_ j ~P U_ j e. A ( { j } X. B )
271 nfcv 
 |-  F/_ j Fin
272 270 271 nfin 
 |-  F/_ j ( ~P U_ j e. A ( { j } X. B ) i^i Fin )
273 269 272 nfel 
 |-  F/ j c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin )
274 268 273 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 ) )
275 simpll 
 |-  ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ph )
276 78 233 syl 
 |-  ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c C_ A )
277 276 sselda 
 |-  ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> j e. A )
278 275 277 159 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 ) )
279 278 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 ) )
280 279 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 ) )
281 280 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 ) ) )
282 274 281 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 ) )
283 15 251 240 282 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 ) )
284 14 283 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* )
285 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 ) ) )
286 28 273 nfan 
 |-  F/ j ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) )
287 id 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> c C_ U_ j e. A ( { j } X. B ) )
288 xpss 
 |-  ( { j } X. B ) C_ ( _V X. _V )
289 288 rgenw 
 |-  A. j e. A ( { j } X. B ) C_ ( _V X. _V )
290 iunss 
 |-  ( U_ j e. A ( { j } X. B ) C_ ( _V X. _V ) <-> A. j e. A ( { j } X. B ) C_ ( _V X. _V ) )
291 289 290 mpbir 
 |-  U_ j e. A ( { j } X. B ) C_ ( _V X. _V )
292 291 a1i 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> U_ j e. A ( { j } X. B ) C_ ( _V X. _V ) )
293 287 292 sstrd 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> c C_ ( _V X. _V ) )
294 78 293 syl 
 |-  ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> c C_ ( _V X. _V ) )
295 df-rel 
 |-  ( Rel c <-> c C_ ( _V X. _V ) )
296 294 295 sylibr 
 |-  ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> Rel c )
297 1 286 15 2 296 19 17 49 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 ) ) ) ) )
298 nfcv 
 |-  F/_ j dom c
299 234 a1i 
 |-  ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c e. _V )
300 275 adantr 
 |-  ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. ( c " { j } ) ) -> ph )
301 277 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 )
302 78 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 ) )
303 imass1 
 |-  ( c C_ U_ j e. A ( { j } X. B ) -> ( c " { j } ) C_ ( U_ j e. A ( { j } X. B ) " { j } ) )
304 302 303 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 } ) )
305 3 4 iunsnima 
 |-  ( ( ph /\ j e. A ) -> ( U_ j e. A ( { j } X. B ) " { j } ) = B )
306 275 277 305 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 )
307 304 306 sseqtrd 
 |-  ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ( c " { j } ) C_ B )
308 307 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 )
309 300 301 308 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 ) )
310 309 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 ) )
311 imaexg 
 |-  ( c e. _V -> ( c " { j } ) e. _V )
312 23 311 ax-mp 
 |-  ( c " { j } ) e. _V
313 nfcv 
 |-  F/_ k ( c " { j } )
314 313 esumcl 
 |-  ( ( ( c " { j } ) e. _V /\ A. k e. ( c " { j } ) C e. ( 0 [,] +oo ) ) -> sum* k e. ( c " { j } ) C e. ( 0 [,] +oo ) )
315 312 314 mpan 
 |-  ( A. k e. ( c " { j } ) C e. ( 0 [,] +oo ) -> sum* k e. ( c " { j } ) C e. ( 0 [,] +oo ) )
316 310 315 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 ) )
317 nfv 
 |-  F/ k ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c )
318 275 277 4 syl2anc 
 |-  ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> B e. W )
319 275 adantr 
 |-  ( ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) /\ k e. B ) -> ph )
320 277 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 )
321 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 )
322 319 320 321 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 ) )
323 317 318 322 307 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 )
324 286 298 299 316 278 323 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 )
325 19 239 syl 
 |-  ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) -> dom c e. Fin )
326 286 298 325 316 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 ) ) )
327 19 adantr 
 |-  ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> c e. Fin )
328 imafi2 
 |-  ( c e. Fin -> ( c " { j } ) e. Fin )
329 327 328 syl 
 |-  ( ( ( ph /\ c e. ( ~P U_ j e. A ( { j } X. B ) i^i Fin ) ) /\ j e. dom c ) -> ( c " { j } ) e. Fin )
330 317 313 329 309 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 ) ) )
331 286 330 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 ) ) ) )
332 331 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 ) ) ) ) )
333 326 332 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 ) ) ) ) )
334 286 298 325 278 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 ) ) )
335 324 333 334 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 ) ) )
336 297 335 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 ) ) )
337 336 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 ) ) )
338 337 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 ) ) )
339 250 267 284 285 338 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 ) ) )
340 247 249 339 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 )
341 340 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 )
342 215 218 219 341 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 )
343 54 87 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 ) ) )
344 343 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 ) ) )
345 344 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 ) ) )
346 206 342 345 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 )
347 7 132 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 ) )
348 347 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 )
349 breq2 
 |-  ( t = u -> ( s < t <-> s < u ) )
350 349 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 )
351 348 350 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 )
352 346 351 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 )
353 7 133 194 352 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* , < ) )
354 nfcv 
 |-  F/_ j A
355 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 ) ) )
356 28 354 3 159 355 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* , < ) )
357 353 356 180 3eqtr4d 
 |-  ( ph -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) F )