Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esum2d Structured version   Unicode version

Theorem esum2d 28916
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.)
Hypotheses
Ref Expression
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
Ref Expression
esum2d  |-  ( ph  -> Σ* j  e.  AΣ* k  e.  B C  = Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F )
Distinct variable groups:    j, k, A, z    z, C    B, k, z    j, F    j, W, k    ph, j, k, z
Allowed substitution hints:    B( j)    C( j, k)    F( z, k)    V( z, j, k)    W( z)

Proof of Theorem esum2d
Dummy variables  t 
a  c  r  s  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrltso 11442 . . . 4  |-  <  Or  RR*
21a1i 11 . . 3  |-  ( ph  ->  <  Or  RR* )
3 nfv 1752 . . . . . . . . 9  |-  F/ c
ph
4 nfcv 2585 . . . . . . . . . 10  |-  F/_ c
s
5 nfmpt1 4511 . . . . . . . . . . 11  |-  F/_ c
( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )
65nfrn 5094 . . . . . . . . . 10  |-  F/_ c ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )
74, 6nfel 2598 . . . . . . . . 9  |-  F/ c  s  e.  ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
83, 7nfan 1985 . . . . . . . 8  |-  F/ c ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )
9 iccssxr 11719 . . . . . . . . . . . . . 14  |-  ( 0 [,] +oo )  C_  RR*
10 xrge0base 28448 . . . . . . . . . . . . . . 15  |-  ( 0 [,] +oo )  =  ( Base `  ( RR*ss  ( 0 [,] +oo ) ) )
11 xrge0cmn 19003 . . . . . . . . . . . . . . . 16  |-  ( RR*ss  ( 0 [,] +oo ) )  e. CMnd
1211a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( RR*ss  (
0 [,] +oo )
)  e. CMnd )
13 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) )
1413elin2d 28147 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  c  e.  Fin )
15 simpll 759 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  z  e.  c )  ->  ph )
1613elin1d 28146 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  c  e.  ~P U_ j  e.  A  ( { j }  X.  B ) )
1716adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) )
18 vex 3085 . . . . . . . . . . . . . . . . . . . 20  |-  c  e. 
_V
1918elpw 3986 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  ~P U_ j  e.  A  ( {
j }  X.  B
)  <->  c  C_  U_ j  e.  A  ( {
j }  X.  B
) )
2017, 19sylib 200 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) )
21 simpr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  z  e.  c )  ->  z  e.  c )
2220, 21sseldd 3466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
23 nfv 1752 . . . . . . . . . . . . . . . . . . 19  |-  F/ j
ph
24 nfcv 2585 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ j
z
25 nfiu1 4327 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ j U_ j  e.  A  ( { j }  X.  B )
2624, 25nfel 2598 . . . . . . . . . . . . . . . . . . 19  |-  F/ j  z  e.  U_ j  e.  A  ( {
j }  X.  B
)
2723, 26nfan 1985 . . . . . . . . . . . . . . . . . 18  |-  F/ j ( ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )
28 nfv 1752 . . . . . . . . . . . . . . . . . . 19  |-  F/ k ( ( ( ph  /\  z  e.  U_ j  e.  A  ( {
j }  X.  B
) )  /\  j  e.  A )  /\  z  e.  ( { j }  X.  B ) )
29 esum2d.0 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ k F
30 nfcv 2585 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ k
( 0 [,] +oo )
3129, 30nfel 2598 . . . . . . . . . . . . . . . . . . 19  |-  F/ k  F  e.  ( 0 [,] +oo )
32 esum2d.1 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  <. j ,  k
>.  ->  F  =  C )
3332adantl 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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 )
34 simp-5l 777 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 )
35 simp-4r 776 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 )
36 simplr 761 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 )
37 esum2d.4 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  C  e.  ( 0 [,] +oo ) )
3834, 35, 36, 37syl12anc 1263 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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 ) )
3933, 38eqeltrd 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
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 ) )
40 elsnxp 5395 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  A  ->  (
z  e.  ( { j }  X.  B
)  <->  E. k  e.  B  z  =  <. j ,  k >. ) )
4140biimpa 487 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( j  e.  A  /\  z  e.  ( {
j }  X.  B
) )  ->  E. k  e.  B  z  =  <. j ,  k >.
)
4241adantll 719 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 >. )
4328, 31, 39, 42r19.29af2 2967 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  /\  j  e.  A )  /\  z  e.  ( { j }  X.  B ) )  ->  F  e.  ( 0 [,] +oo )
)
44 simpr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  -> 
z  e.  U_ j  e.  A  ( {
j }  X.  B
) )
45 eliun 4302 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  U_ j  e.  A  ( { j }  X.  B )  <->  E. j  e.  A  z  e.  ( {
j }  X.  B
) )
4644, 45sylib 200 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  ->  E. j  e.  A  z  e.  ( {
j }  X.  B
) )
4727, 43, 46r19.29af 2969 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  ->  F  e.  ( 0 [,] +oo ) )
4815, 22, 47syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  z  e.  c )  ->  F  e.  ( 0 [,] +oo ) )
4948ralrimiva 2840 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  A. z  e.  c  F  e.  ( 0 [,] +oo ) )
5010, 12, 14, 49gsummptcl 17592 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e.  ( 0 [,] +oo ) )
519, 50sseldi 3463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
RR* )
5251ralrimiva 2840 . . . . . . . . . . . 12  |-  ( ph  ->  A. c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) )  e. 
RR* )
53 eqid 2423 . . . . . . . . . . . . 13  |-  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  =  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )
5453rnmptss 6065 . . . . . . . . . . . 12  |-  ( A. c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
RR*  ->  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) 
C_  RR* )
5552, 54syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) 
C_  RR* )
5655ad3antrrr 735 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) 
C_  RR* )
57 simpllr 768 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) )
5856, 57sseldd 3466 . . . . . . . . 9  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  e.  RR* )
59 esum2d.2 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  V )
60 snex 4660 . . . . . . . . . . . . . . 15  |-  { j }  e.  _V
61 esum2d.3 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  A )  ->  B  e.  W )
62 xpexg 6605 . . . . . . . . . . . . . . 15  |-  ( ( { j }  e.  _V  /\  B  e.  W
)  ->  ( {
j }  X.  B
)  e.  _V )
6360, 61, 62sylancr 668 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  A )  ->  ( { j }  X.  B )  e.  _V )
6463ralrimiva 2840 . . . . . . . . . . . . 13  |-  ( ph  ->  A. j  e.  A  ( { j }  X.  B )  e.  _V )
65 iunexg 6781 . . . . . . . . . . . . 13  |-  ( ( A  e.  V  /\  A. j  e.  A  ( { j }  X.  B )  e.  _V )  ->  U_ j  e.  A  ( { j }  X.  B )  e.  _V )
6659, 64, 65syl2anc 666 . . . . . . . . . . . 12  |-  ( ph  ->  U_ j  e.  A  ( { j }  X.  B )  e.  _V )
6747ralrimiva 2840 . . . . . . . . . . . 12  |-  ( ph  ->  A. z  e.  U_  j  e.  A  ( { j }  X.  B ) F  e.  ( 0 [,] +oo ) )
68 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ z U_ j  e.  A  ( { j }  X.  B )
6968esumcl 28853 . . . . . . . . . . . 12  |-  ( (
U_ j  e.  A  ( { j }  X.  B )  e.  _V  /\ 
A. z  e.  U_  j  e.  A  ( { j }  X.  B ) F  e.  ( 0 [,] +oo ) )  -> Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e.  ( 0 [,] +oo ) )
7066, 67, 69syl2anc 666 . . . . . . . . . . 11  |-  ( ph  -> Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e.  ( 0 [,] +oo ) )
719, 70sseldi 3463 . . . . . . . . . 10  |-  ( ph  -> Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e.  RR* )
7271ad3antrrr 735 . . . . . . . . 9  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  -> Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F  e.  RR* )
73 simpr 463 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )
74 nfv 1752 . . . . . . . . . . . . . 14  |-  F/ z ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)
75 nfcv 2585 . . . . . . . . . . . . . 14  |-  F/_ z
c
7674, 75, 14, 48esumgsum 28868 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  -> Σ* z  e.  c F  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
7766adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  U_ j  e.  A  ( { j }  X.  B )  e.  _V )
7847adantlr 720 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
7916, 19sylib 200 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  c  C_  U_ j  e.  A  ( {
j }  X.  B
) )
8074, 77, 78, 79esummono 28877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  -> Σ* z  e.  c F  <_ Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F )
8176, 80eqbrtrrd 4444 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
8281adantlr 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
8382adantr 467 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
8473, 83eqbrtrd 4442 . . . . . . . . 9  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
85 xrlenlt 9701 . . . . . . . . . 10  |-  ( ( s  e.  RR*  /\ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e. 
RR* )  ->  (
s  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  <->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
s ) )
8685biimpa 487 . . . . . . . . 9  |-  ( ( ( s  e.  RR*  /\ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e.  RR* )  /\  s  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
s )
8758, 72, 84, 86syl21anc 1264 . . . . . . . 8  |-  ( ( ( ( ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  s  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
s )
88 simpr 463 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) )  ->  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) )
89 ovex 6331 . . . . . . . . . 10  |-  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
_V
9053, 89elrnmpti 5102 . . . . . . . . 9  |-  ( s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  <->  E. c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) s  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )
9188, 90sylib 200 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) )  ->  E. c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
s  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
928, 87, 91r19.29af 2969 . . . . . . 7  |-  ( (
ph  /\  s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) )  ->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
s )
9392ralrimiva 2840 . . . . . 6  |-  ( ph  ->  A. s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )  -. Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F  <  s
)
94 nfv 1752 . . . . . . . . 9  |-  F/ c ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F )
95 nfv 1752 . . . . . . . . . 10  |-  F/ c  s  <  t
966, 95nfrex 2889 . . . . . . . . 9  |-  F/ c E. t  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t
9776adantlr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  e.  RR* )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  -> Σ* z  e.  c F  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
9897adantlr 720 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  -> Σ* z  e.  c F  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
9998adantr 467 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  -> Σ* z  e.  c F  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
100 simplr 761 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  ->  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)
10189a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
_V )
10253elrnmpt1 5100 . . . . . . . . . . . 12  |-  ( ( c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  /\  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
_V )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )
103100, 101, 102syl2anc 666 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )
10499, 103eqeltrd 2511 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  -> Σ* z  e.  c F  e.  ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )
105 simpr 463 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  /\  t  = Σ* z  e.  c F
)  ->  t  = Σ* z  e.  c F )
106105breq2d 4433 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  /\  t  = Σ* z  e.  c F
)  ->  ( s  <  t  <->  s  < Σ* z  e.  c F ) )
107 simpr 463 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  ->  s  < Σ* z  e.  c F )
108104, 106, 107rspcedvd 3188 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  s  < Σ* z  e.  c F )  ->  E. t  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t )
109 nfv 1752 . . . . . . . . . . 11  |-  F/ z ( ph  /\  s  e.  RR* )
110 nfcv 2585 . . . . . . . . . . . 12  |-  F/_ z
s
111 nfcv 2585 . . . . . . . . . . . 12  |-  F/_ z  <
11268nfesum1 28863 . . . . . . . . . . . 12  |-  F/_ zΣ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F
113110, 111, 112nfbr 4466 . . . . . . . . . . 11  |-  F/ z  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F
114109, 113nfan 1985 . . . . . . . . . 10  |-  F/ z ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F )
11566ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  U_ j  e.  A  ( {
j }  X.  B
)  e.  _V )
116473ad2antr3 1173 . . . . . . . . . . 11  |-  ( (
ph  /\  ( s  e.  RR*  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) ) )  ->  F  e.  ( 0 [,] +oo ) )
1171163anassrs 1229 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* 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 761 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  s  e.  RR* )
119 simpr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
120114, 115, 117, 118, 119esumlub 28883 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* 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  < Σ* z  e.  c F )
12194, 96, 108, 120r19.29af2 2967 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* 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*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t )
122121ex 436 . . . . . . 7  |-  ( (
ph  /\  s  e.  RR* )  ->  ( s  < Σ* 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*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) )
123122ralrimiva 2840 . . . . . 6  |-  ( ph  ->  A. s  e.  RR*  ( s  < Σ* 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) )
12493, 123jca 535 . . . . 5  |-  ( ph  ->  ( A. s  e. 
ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  -. Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F  <  s  /\  A. s  e.  RR*  ( s  < Σ* 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) ) )
125 simpr 463 . . . . . . . . . 10  |-  ( (
ph  /\  r  = Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  r  = Σ* z  e. 
U_ j  e.  A  ( { j }  X.  B ) F )
126125breq1d 4431 . . . . . . . . 9  |-  ( (
ph  /\  r  = Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  ( r  < 
s  <-> Σ*
z  e.  U_ j  e.  A  ( {
j }  X.  B
) F  <  s
) )
127126notbid 296 . . . . . . . 8  |-  ( (
ph  /\  r  = Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  ( -.  r  <  s  <->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
s ) )
128127ralbidv 2865 . . . . . . 7  |-  ( (
ph  /\  r  = Σ* 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*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  -.  r  <  s  <->  A. s  e.  ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  -. Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F  <  s
) )
129125breq2d 4433 . . . . . . . . 9  |-  ( (
ph  /\  r  = Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  ( s  < 
r  <->  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F ) )
130129imbi1d 319 . . . . . . . 8  |-  ( (
ph  /\  r  = Σ* 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*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t )  <-> 
( s  < Σ* 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) ) )
131130ralbidv 2865 . . . . . . 7  |-  ( (
ph  /\  r  = Σ* 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*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t )  <->  A. s  e.  RR*  (
s  < Σ* 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) ) )
132128, 131anbi12d 716 . . . . . 6  |-  ( (
ph  /\  r  = Σ* 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*ss  ( 0 [,] +oo ) )  gsumg  ( 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) )  <->  ( A. s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  -. Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F  <  s  /\  A. s  e.  RR*  ( s  < Σ* 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) ) ) )
13371, 132rspcedv 3187 . . . . 5  |-  ( ph  ->  ( ( A. s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  -. Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F  <  s  /\  A. s  e.  RR*  ( s  < Σ* 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( 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*ss  (
0 [,] +oo )
)  gsumg  ( 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) ) ) )
134124, 133mpd 15 . . . 4  |-  ( ph  ->  E. r  e.  RR*  ( A. s  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) s  <  t ) ) )
1352, 134supcl 7976 . . 3  |-  ( ph  ->  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  e.  RR* )
136 nfv 1752 . . . . 5  |-  F/ a
ph
137 nfcv 2585 . . . . . 6  |-  F/_ a
s
138 nfmpt1 4511 . . . . . . 7  |-  F/_ a
( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
139138nfrn 5094 . . . . . 6  |-  F/_ a ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
140137, 139nfel 2598 . . . . 5  |-  F/ a  s  e.  ran  (
a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
141136, 140nfan 1985 . . . 4  |-  F/ a ( ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
142 simpr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  e.  ( ~P A  i^i  Fin ) )
143 simpll 759 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  ->  ph )
144142elin1d 28146 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  e.  ~P A )
145 elpwi 3989 . . . . . . . . . . . . . . 15  |-  ( a  e.  ~P A  -> 
a  C_  A )
146144, 145syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  C_  A )
147146sselda 3465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  ->  j  e.  A )
148143, 147, 61syl2anc 666 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  ->  B  e.  W )
149143adantrr 722 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  ph )
150147adantrr 722 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  j  e.  A )
151 simprr 765 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  k  e.  B )
152149, 150, 151, 37syl12anc 1263 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  C  e.  ( 0 [,] +oo ) )
153142elin2d 28147 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  e.  Fin )
15429, 32, 142, 148, 152, 153esum2dlem 28915 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  -> Σ* j  e.  aΣ* k  e.  B C  = Σ* z  e.  U_ j  e.  a  ( { j }  X.  B ) F )
155 nfv 1752 . . . . . . . . . . . 12  |-  F/ j ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )
156 nfcv 2585 . . . . . . . . . . . 12  |-  F/_ j
a
15737anassrs 653 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  A )  /\  k  e.  B )  ->  C  e.  ( 0 [,] +oo ) )
158157ralrimiva 2840 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  A )  ->  A. k  e.  B  C  e.  ( 0 [,] +oo ) )
159 nfcv 2585 . . . . . . . . . . . . . . 15  |-  F/_ k B
160159esumcl 28853 . . . . . . . . . . . . . 14  |-  ( ( B  e.  W  /\  A. k  e.  B  C  e.  ( 0 [,] +oo ) )  -> Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
16161, 158, 160syl2anc 666 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  A )  -> Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
162143, 147, 161syl2anc 666 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  -> Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
163155, 156, 153, 162esumgsum 28868 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  -> Σ* j  e.  aΣ* k  e.  B C  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
164154, 163eqtr3d 2466 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  -> Σ* z  e.  U_ j  e.  a  ( { j }  X.  B ) F  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
165 nfv 1752 . . . . . . . . . . 11  |-  F/ z ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )
16666adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  U_ j  e.  A  ( {
j }  X.  B
)  e.  _V )
16747adantlr 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  ->  F  e.  ( 0 [,] +oo ) )
168 iunss1 4309 . . . . . . . . . . . 12  |-  ( a 
C_  A  ->  U_ j  e.  a  ( {
j }  X.  B
)  C_  U_ j  e.  A  ( { j }  X.  B ) )
169146, 168syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  U_ j  e.  a  ( {
j }  X.  B
)  C_  U_ j  e.  A  ( { j }  X.  B ) )
170165, 166, 167, 169esummono 28877 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  -> Σ* z  e.  U_ j  e.  a  ( { j }  X.  B ) F  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
171164, 170eqbrtrrd 4444 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
17211a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  ( RR*ss  ( 0 [,] +oo ) )  e. CMnd )
173162ralrimiva 2840 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  A. j  e.  a Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
17410, 172, 153, 173gsummptcl 17592 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  e.  ( 0 [,] +oo )
)
1759, 174sseldi 3463 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  e.  RR* )
17671adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  -> Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e. 
RR* )
177 xrlenlt 9701 . . . . . . . . . 10  |-  ( ( ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  e.  RR*  /\ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e.  RR* )  ->  ( ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  <->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
178175, 176, 177syl2anc 666 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  (
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  <->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
179171, 178mpbid 214 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  -. Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
180 nfv 1752 . . . . . . . . . . 11  |-  F/ z
ph
181 eqidd 2424 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )
182180, 68, 66, 47, 181esumval 28869 . . . . . . . . . 10  |-  ( ph  -> Σ* 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)
183182adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  -> Σ* 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*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)
184183breq1d 4431 . . . . . . . 8  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  (Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  < 
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  <->  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
185179, 184mtbid 302 . . . . . . 7  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  -.  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
186185adantlr 720 . . . . . 6  |-  ( ( ( ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* 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*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
187186adantr 467 . . . . 5  |-  ( ( ( ( ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  s  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  ->  -.  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
188 simpr 463 . . . . . . 7  |-  ( ( ( ( ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  s  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  -> 
s  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
189188breq2d 4433 . . . . . 6  |-  ( ( ( ( ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  s  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  -> 
( sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  s  <->  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
190189notbid 296 . . . . 5  |-  ( ( ( ( ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  s  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  -> 
( -.  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  s  <->  -.  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
191187, 190mpbird 236 . . . 4  |-  ( ( ( ( ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  s  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  ->  -.  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  s )
192 eqid 2423 . . . . . . 7  |-  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  =  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
193 ovex 6331 . . . . . . 7  |-  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  e.  _V
194192, 193elrnmpti 5102 . . . . . 6  |-  ( s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  <->  E. a  e.  ( ~P A  i^i  Fin ) s  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
195194biimpi 198 . . . . 5  |-  ( s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )  ->  E. a  e.  ( ~P A  i^i  Fin )
s  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
196195adantl 468 . . . 4  |-  ( (
ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )  ->  E. a  e.  ( ~P A  i^i  Fin ) s  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
197141, 191, 196r19.29af 2969 . . 3  |-  ( (
ph  /\  s  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )  ->  -.  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )  <  s )
1984nfel1 2601 . . . . . . . . 9  |-  F/ c  s  e.  RR*
199 nfcv 2585 . . . . . . . . . 10  |-  F/_ c  <
200 nfcv 2585 . . . . . . . . . . 11  |-  F/_ c RR*
2016, 200, 199nfsup 7969 . . . . . . . . . 10  |-  F/_ c sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
2024, 199, 201nfbr 4466 . . . . . . . . 9  |-  F/ c  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
203198, 202nfan 1985 . . . . . . . 8  |-  F/ c ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)
2043, 203nfan 1985 . . . . . . 7  |-  F/ c ( ph  /\  (
s  e.  RR*  /\  s  <  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )
205 nfcv 2585 . . . . . . . 8  |-  F/_ c
u
206205, 6nfel 2598 . . . . . . 7  |-  F/ c  u  e.  ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
207204, 206nfan 1985 . . . . . 6  |-  F/ c ( ( ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )
208 nfv 1752 . . . . . 6  |-  F/ c  s  <  u
209207, 208nfan 1985 . . . . 5  |-  F/ c ( ( ( ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )
210 simp-5l 777 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  ph )
211 simpr1l 1063 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
s  e.  RR*  /\  s  <  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )  /\  ( s  < 
u  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  /\  u  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ) )  ->  s  e.  RR* )
2122113anassrs 1229 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  ( s  <  u  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  /\  u  =  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  ->  s  e.  RR* )
2132123anassrs 1229 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  e.  RR* )
214210, 213jca 535 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  ( ph  /\  s  e.  RR* ) )
215 simpr1r 1064 . . . . . . . . 9  |-  ( (
ph  /\  ( (
s  e.  RR*  /\  s  <  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )  /\  ( s  < 
u  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  /\  u  =  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ) )  ->  s  <  sup ( ran  (
c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)
2162153anassrs 1229 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  ( s  <  u  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  /\  u  =  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) )  ->  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)
2172163anassrs 1229 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
)
218214, 217jca 535 . . . . . 6  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( 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*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )
219 simpllr 768 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  <  u
)
220 simpr 463 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  u  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( z  e.  c 
|->  F ) ) )
221219, 220breqtrd 4446 . . . . . 6  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  s  <  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
222 simplr 761 . . . . . 6  |-  ( ( ( ( ( (
ph  /\  ( s  e.  RR*  /\  s  <  sup ( ran  ( c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) ) ,  RR* ,  <  )
) )  /\  u  e.  ran  ( c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )  |->  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) ) )  /\  s  < 
u )  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  u  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) ) )  ->  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )
223 simpr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( 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 ) )
224223elin1d 28146 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( 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 3989 . . . . . . . . . . 11  |-  ( c  e.  ~P U_ j  e.  A  ( {
j }  X.  B
)  ->  c  C_  U_ j  e.  A  ( { j }  X.  B ) )
226 dmss 5051 . . . . . . . . . . . . . 14  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  C_  dom  U_ j  e.  A  ( {
j }  X.  B
) )
227 dmiun 5060 . . . . . . . . . . . . . 14  |-  dom  U_ j  e.  A  ( {
j }  X.  B
)  =  U_ j  e.  A  dom  ( { j }  X.  B
)
228226, 227syl6sseq 3511 . . . . . . . . . . . . 13  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  C_  U_ j  e.  A  dom  ( { j }  X.  B
) )
229 dmxpss 5285 . . . . . . . . . . . . . . . . 17  |-  dom  ( { j }  X.  B )  C_  { j }
230229a1i 11 . . . . . . . . . . . . . . . 16  |-  ( j  e.  A  ->  dom  ( { j }  X.  B )  C_  { j } )
231 snssi 4142 . . . . . . . . . . . . . . . 16  |-  ( j  e.  A  ->  { j }  C_  A )
232230, 231sstrd 3475 . . . . . . . . . . . . . . 15  |-  ( j  e.  A  ->  dom  ( { j }  X.  B )  C_  A
)
233232rgen 2786 . . . . . . . . . . . . . 14  |-  A. j  e.  A  dom  ( { j }  X.  B
)  C_  A
234 iunss 4338 . . . . . . . . . . . . . 14  |-  ( U_ j  e.  A  dom  ( { j }  X.  B )  C_  A  <->  A. j  e.  A  dom  ( { j }  X.  B )  C_  A
)
235233, 234mpbir 213 . . . . . . . . . . . . 13  |-  U_ j  e.  A  dom  ( { j }  X.  B
)  C_  A
236228, 235syl6ss 3477 . . . . . . . . . . . 12  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  C_  A )
23718dmex 6738 . . . . . . . . . . . . 13  |-  dom  c  e.  _V
238237elpw 3986 . . . . . . . . . . . 12  |-  ( dom  c  e.  ~P A  <->  dom  c  C_  A )
239236, 238sylibr 216 . . . . . . . . . . 11  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  e.  ~P A
)
240224, 225, 2393syl 18 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  dom  c  e.  ~P A )
241223elin2d 28147 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  c  e.  Fin )
242 dmfi 7858 . . . . . . . . . . 11  |-  ( c  e.  Fin  ->  dom  c  e.  Fin )
243241, 242syl 17 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  dom  c  e.  Fin )
244240, 243elind 3651 . . . . . . . . 9  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( 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 6331 . . . . . . . . . 10  |-  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) )  e.  _V
246245a1i 11 . . . . . . . . 9  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) )  e.  _V )
247 mpteq1 4502 . . . . . . . . . . 11  |-  ( a  =  dom  c  -> 
( j  e.  a 
|-> Σ* k  e.  B C
)  =  ( j  e.  dom  c  |-> Σ* k  e.  B C ) )
248247oveq2d 6319 . . . . . . . . . 10  |-  ( a  =  dom  c  -> 
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) ) )
249192, 248elrnmpt1s 5099 . . . . . . . . 9  |-  ( ( dom  c  e.  ( ~P A  i^i  Fin )  /\  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) )  e.  _V )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) )  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
250244, 246, 249syl2anc 666 . . . . . . . 8  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) )  e.  ran  ( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) ) )
251 simpr 463 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  t  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) ) )  -> 
t  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) ) )
252251breq2d 4433 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  t  =  ( ( RR*ss  ( 0 [,] +oo ) ) 
gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) ) )  -> 
( s  <  t  <->  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  dom  c  |-> Σ* k  e.  B C ) ) ) )
253 simpllr 768 . . . . . . . . 9  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  s  e.  RR* )
25411a1i 11 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( RR*ss  (
0 [,] +oo )
)  e. CMnd )
255 nfcv 2585 . . . . . . . . . . . . . . . 16  |-  F/_ z
( RR*ss  ( 0 [,] +oo ) )
256 nfcv 2585 . . . . . . . . . . . . . . . 16  |-  F/_ z  gsumg
257 nfmpt1 4511 . . . . . . . . . . . . . . . 16  |-  F/_ z
( z  e.  c 
|->  F )
258255, 256, 257nfov 6329 . . . . . . . . . . . . . . 15  |-  F/_ z
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) )
259110, 111, 258nfbr 4466 . . . . . . . . . . . . . 14  |-  F/ z  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )
260109, 259nfan 1985 . . . . . . . . . . . . 13  |-  F/ z ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
261 nfv 1752 . . . . . . . . . . . . 13  |-  F/ z  c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )
262260, 261nfan 1985 . . . . . . . . . . . 12  |-  F/ z ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )
263 simp-4l 775 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  z  e.  c )  ->  ph )
264224, 225syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( 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
) )
265264sselda 3465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( 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 ) )
266263, 265, 47syl2anc 666 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  z  e.  c )  ->  F  e.  ( 0 [,] +oo ) )
267266ex 436 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( z  e.  c  ->  F  e.  ( 0 [,] +oo ) ) )
268262, 267ralrimi 2826 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( 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 ) )
26910, 254, 241, 268gsummptcl 17592 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e.  ( 0 [,] +oo ) )
2709, 269sseldi 3463 . . . . . . . . 9  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
RR* )
271 nfv 1752 . . . . . . . . . . . . 13  |-  F/ j ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
272 nfcv 2585 . . . . . . . . . . . . . 14  |-  F/_ j
c
27325nfpw 3992 . . . . . . . . . . . . . . 15  |-  F/_ j ~P U_ j  e.  A  ( { j }  X.  B )
274 nfcv 2585 . . . . . . . . . . . . . . 15  |-  F/_ j Fin
275273, 274nfin 3670 . . . . . . . . . . . . . 14  |-  F/_ j
( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
276272, 275nfel 2598 . . . . . . . . . . . . 13  |-  F/ j  c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )
277271, 276nfan 1985 . . . . . . . . . . . 12  |-  F/ j ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )
278 simpll 759 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  j  e.  dom  c )  ->  ph )
27979, 236syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  dom  c  C_  A )
280279sselda 3465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  j  e.  dom  c )  ->  j  e.  A )
281278, 280, 161syl2anc 666 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
282281adantllr 724 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  s  e.  RR* )  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  /\  j  e.  dom  c )  -> Σ* k  e.  B C  e.  ( 0 [,] +oo )
)
283282adantllr 724 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  (