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

Theorem esum2d 28322
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 11350 . . . 4  |-  <  Or  RR*
21a1i 11 . . 3  |-  ( ph  ->  <  Or  RR* )
3 nfv 1712 . . . . . . . . 9  |-  F/ c
ph
4 nfcv 2616 . . . . . . . . . 10  |-  F/_ c
s
5 nfmpt1 4528 . . . . . . . . . . 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 5234 . . . . . . . . . 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 2629 . . . . . . . . 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 1933 . . . . . . . 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 11610 . . . . . . . . . . . . . 14  |-  ( 0 [,] +oo )  C_  RR*
10 xrge0base 27907 . . . . . . . . . . . . . . 15  |-  ( 0 [,] +oo )  =  ( Base `  ( RR*ss  ( 0 [,] +oo ) ) )
11 xrge0cmn 18655 . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 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 27618 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  c  e.  Fin )
15 simpll 751 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  z  e.  c )  ->  ph )
1613elin1d 27617 . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . 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 3109 . . . . . . . . . . . . . . . . . . . 20  |-  c  e. 
_V
1918elpw 4005 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  ~P U_ j  e.  A  ( {
j }  X.  B
)  <->  c  C_  U_ j  e.  A  ( {
j }  X.  B
) )
2017, 19sylib 196 . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  z  e.  c )  ->  z  e.  c )
2220, 21sseldd 3490 . . . . . . . . . . . . . . . . 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 1712 . . . . . . . . . . . . . . . . . . 19  |-  F/ j
ph
24 nfcv 2616 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ j
z
25 nfiu1 4345 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ j U_ j  e.  A  ( { j }  X.  B )
2624, 25nfel 2629 . . . . . . . . . . . . . . . . . . 19  |-  F/ j  z  e.  U_ j  e.  A  ( {
j }  X.  B
)
2723, 26nfan 1933 . . . . . . . . . . . . . . . . . 18  |-  F/ j ( ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )
28 nfv 1712 . . . . . . . . . . . . . . . . . . 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 2616 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ k
( 0 [,] +oo )
3129, 30nfel 2629 . . . . . . . . . . . . . . . . . . 19  |-  F/ k  F  e.  ( 0 [,] +oo )
32 esum2d.1 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  <. j ,  k
>.  ->  F  =  C )
3332adantl 464 . . . . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . . . . . . . . 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 753 . . . . . . . . . . . . . . . . . . . . 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 1224 . . . . . . . . . . . . . . . . . . . 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 2542 . . . . . . . . . . . . . . . . . . 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 27684 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  A  ->  (
z  e.  ( { j }  X.  B
)  <->  E. k  e.  B  z  =  <. j ,  k >. ) )
4140biimpa 482 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( j  e.  A  /\  z  e.  ( {
j }  X.  B
) )  ->  E. k  e.  B  z  =  <. j ,  k >.
)
4241adantll 711 . . . . . . . . . . . . . . . . . . 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 2992 . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  -> 
z  e.  U_ j  e.  A  ( {
j }  X.  B
) )
45 eliun 4320 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  U_ j  e.  A  ( { j }  X.  B )  <->  E. j  e.  A  z  e.  ( {
j }  X.  B
) )
4644, 45sylib 196 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  ->  E. j  e.  A  z  e.  ( {
j }  X.  B
) )
4727, 43, 46r19.29af 2994 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  ->  F  e.  ( 0 [,] +oo ) )
4815, 22, 47syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  z  e.  c )  ->  F  e.  ( 0 [,] +oo ) )
4948ralrimiva 2868 . . . . . . . . . . . . . . 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 17190 . . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . 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 2868 . . . . . . . . . . . 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 2454 . . . . . . . . . . . . 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 6036 . . . . . . . . . . . 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 16 . . . . . . . . . . 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 727 . . . . . . . . . 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 758 . . . . . . . . . 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 3490 . . . . . . . . 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 4678 . . . . . . . . . . . . . . 15  |-  { j }  e.  _V
61 esum2d.3 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  A )  ->  B  e.  W )
62 xpexg 6575 . . . . . . . . . . . . . . 15  |-  ( ( { j }  e.  _V  /\  B  e.  W
)  ->  ( {
j }  X.  B
)  e.  _V )
6360, 61, 62sylancr 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  A )  ->  ( { j }  X.  B )  e.  _V )
6463ralrimiva 2868 . . . . . . . . . . . . 13  |-  ( ph  ->  A. j  e.  A  ( { j }  X.  B )  e.  _V )
65 iunexg 6749 . . . . . . . . . . . . 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 659 . . . . . . . . . . . 12  |-  ( ph  ->  U_ j  e.  A  ( { j }  X.  B )  e.  _V )
6747ralrimiva 2868 . . . . . . . . . . . 12  |-  ( ph  ->  A. z  e.  U_  j  e.  A  ( { j }  X.  B ) F  e.  ( 0 [,] +oo ) )
68 nfcv 2616 . . . . . . . . . . . . 13  |-  F/_ z U_ j  e.  A  ( { j }  X.  B )
6968esumcl 28259 . . . . . . . . . . . 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 659 . . . . . . . . . . 11  |-  ( ph  -> Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e.  ( 0 [,] +oo ) )
719, 70sseldi 3487 . . . . . . . . . 10  |-  ( ph  -> Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e.  RR* )
7271ad3antrrr 727 . . . . . . . . 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 459 . . . . . . . . . 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 1712 . . . . . . . . . . . . . 14  |-  F/ z ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)
75 nfcv 2616 . . . . . . . . . . . . . 14  |-  F/_ z
c
7674, 75, 14, 48esumgsum 28274 . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . 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 196 . . . . . . . . . . . . . 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 28283 . . . . . . . . . . . . 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 4461 . . . . . . . . . . . 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 712 . . . . . . . . . . 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 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 ) ) )  ->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  <_ Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )
8473, 83eqbrtrd 4459 . . . . . . . . 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 9641 . . . . . . . . . 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 482 . . . . . . . . 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 1225 . . . . . . . 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 459 . . . . . . . . 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 6298 . . . . . . . . . 10  |-  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )  e. 
_V
9053, 89elrnmpti 5242 . . . . . . . . 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 196 . . . . . . . 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 2994 . . . . . . 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 2868 . . . . . 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 1712 . . . . . . . . 9  |-  F/ c ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F )
95 nfv 1712 . . . . . . . . . 10  |-  F/ c  s  <  t
966, 95nfrex 2917 . . . . . . . . 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 712 . . . . . . . . . . . . 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 712 . . . . . . . . . . . 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 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 )  -> Σ* z  e.  c F  =  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
100 simplr 753 . . . . . . . . . . . 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 5240 . . . . . . . . . . . 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 659 . . . . . . . . . . 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 2542 . . . . . . . . . 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 459 . . . . . . . . . . 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 4451 . . . . . . . . . 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 459 . . . . . . . . . 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 3212 . . . . . . . . 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 1712 . . . . . . . . . . 11  |-  F/ z ( ph  /\  s  e.  RR* )
110 nfcv 2616 . . . . . . . . . . . 12  |-  F/_ z
s
111 nfcv 2616 . . . . . . . . . . . 12  |-  F/_ z  <
11268nfesum1 28269 . . . . . . . . . . . 12  |-  F/_ zΣ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F
113110, 111, 112nfbr 4483 . . . . . . . . . . 11  |-  F/ z  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F
114109, 113nfan 1933 . . . . . . . . . 10  |-  F/ z ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( {
j }  X.  B
) F )
11566ad2antrr 723 . . . . . . . . . 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 1161 . . . . . . . . . . 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 1216 . . . . . . . . . 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 753 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  RR* )  /\  s  < Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F )  ->  s  e.  RR* )
119 simpr 459 . . . . . . . . . 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 28289 . . . . . . . . 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 2992 . . . . . . . 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 432 . . . . . . 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 2868 . . . . . 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 530 . . . . 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 459 . . . . . . . . . 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 4449 . . . . . . . . 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 292 . . . . . . . 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 2893 . . . . . . 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 4451 . . . . . . . . 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 315 . . . . . . . 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 2893 . . . . . . 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 708 . . . . . 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 3211 . . . . 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 7909 . . 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 1712 . . . . 5  |-  F/ a
ph
137 nfcv 2616 . . . . . 6  |-  F/_ a
s
138 nfmpt1 4528 . . . . . . 7  |-  F/_ a
( a  e.  ( ~P A  i^i  Fin )  |->  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) ) )
139138nfrn 5234 . . . . . 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 2629 . . . . 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 1933 . . . 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 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  e.  ( ~P A  i^i  Fin ) )
143 simpll 751 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  ->  ph )
144142elin1d 27617 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  e.  ~P A )
145 elpwi 4008 . . . . . . . . . . . . . . 15  |-  ( a  e.  ~P A  -> 
a  C_  A )
146144, 145syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  C_  A )
147146sselda 3489 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  ->  j  e.  A )
148143, 147, 61syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  ->  B  e.  W )
149143adantrr 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  ph )
150147adantrr 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  j  e.  A )
151 simprr 755 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  k  e.  B )
152149, 150, 151, 37syl12anc 1224 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  (
j  e.  a  /\  k  e.  B )
)  ->  C  e.  ( 0 [,] +oo ) )
153142elin2d 27618 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  a  e.  Fin )
15429, 32, 142, 148, 152, 153esum2dlem 28321 . . . . . . . . . . 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 1712 . . . . . . . . . . . 12  |-  F/ j ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )
156 nfcv 2616 . . . . . . . . . . . 12  |-  F/_ j
a
15737anassrs 646 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  A )  /\  k  e.  B )  ->  C  e.  ( 0 [,] +oo ) )
158157ralrimiva 2868 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  A )  ->  A. k  e.  B  C  e.  ( 0 [,] +oo ) )
159 nfcv 2616 . . . . . . . . . . . . . . 15  |-  F/_ k B
160159esumcl 28259 . . . . . . . . . . . . . 14  |-  ( ( B  e.  W  /\  A. k  e.  B  C  e.  ( 0 [,] +oo ) )  -> Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
16161, 158, 160syl2anc 659 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  A )  -> Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
162143, 147, 161syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  j  e.  a )  -> Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
163155, 156, 153, 162esumgsum 28274 . . . . . . . . . . 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 2497 . . . . . . . . . 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 1712 . . . . . . . . . . 11  |-  F/ z ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )
16666adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  U_ j  e.  A  ( {
j }  X.  B
)  e.  _V )
16747adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ph  /\  a  e.  ( ~P A  i^i  Fin ) )  /\  z  e.  U_ j  e.  A  ( { j }  X.  B ) )  ->  F  e.  ( 0 [,] +oo ) )
168 iunss1 4327 . . . . . . . . . . . 12  |-  ( a 
C_  A  ->  U_ j  e.  a  ( {
j }  X.  B
)  C_  U_ j  e.  A  ( { j }  X.  B ) )
169146, 168syl 16 . . . . . . . . . . 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 28283 . . . . . . . . . 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 4461 . . . . . . . . 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 2868 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  A. j  e.  a Σ* k  e.  B C  e.  ( 0 [,] +oo ) )
17410, 172, 153, 173gsummptcl 17190 . . . . . . . . . . 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 3487 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  e.  RR* )
17671adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  ( ~P A  i^i  Fin ) )  -> Σ* z  e.  U_ j  e.  A  ( { j }  X.  B ) F  e. 
RR* )
177 xrlenlt 9641 . . . . . . . . . 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 659 . . . . . . . . 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 210 . . . . . . . 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 1712 . . . . . . . . . . 11  |-  F/ z
ph
181 eqidd 2455 . . . . . . . . . . 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 28275 . . . . . . . . . 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 463 . . . . . . . . 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 4449 . . . . . . . 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 298 . . . . . . 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 712 . . . . . 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 463 . . . . 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 459 . . . . . . 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 4451 . . . . . 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 292 . . . . 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 232 . . . 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 2454 . . . . . . 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 6298 . . . . . . 7  |-  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( j  e.  a 
|-> Σ* k  e.  B C
) )  e.  _V
194192, 193elrnmpti 5242 . . . . . 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 194 . . . . 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 464 . . . 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 2994 . . 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 2632 . . . . . . . . 9  |-  F/ c  s  e.  RR*
199 nfcv 2616 . . . . . . . . . 10  |-  F/_ c  <
200 nfcv 2616 . . . . . . . . . . 11  |-  F/_ c RR*
2016, 200, 199nfsup 7902 . . . . . . . . . 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 4483 . . . . . . . . 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 1933 . . . . . . . 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 1933 . . . . . . 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 2616 . . . . . . . 8  |-  F/_ c
u
206205, 6nfel 2629 . . . . . . 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 1933 . . . . . 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 1712 . . . . . 6  |-  F/ c  s  <  u
209207, 208nfan 1933 . . . . 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 767 . . . . . . . 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 1051 . . . . . . . . . 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 1216 . . . . . . . . 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 1216 . . . . . . . 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 530 . . . . . . 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 1052 . . . . . . . . 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 1216 . . . . . . . 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 1216 . . . . . . 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 530 . . . . . 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 758 . . . . . . 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 459 . . . . . . 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 4463 . . . . . 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 753 . . . . . 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 459 . . . . . . . . . . . 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 27617 . . . . . . . . . . 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 4008 . . . . . . . . . . 11  |-  ( c  e.  ~P U_ j  e.  A  ( {
j }  X.  B
)  ->  c  C_  U_ j  e.  A  ( { j }  X.  B ) )
226 dmss 5191 . . . . . . . . . . . . . 14  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  C_  dom  U_ j  e.  A  ( {
j }  X.  B
) )
227 dmiun 5200 . . . . . . . . . . . . . 14  |-  dom  U_ j  e.  A  ( {
j }  X.  B
)  =  U_ j  e.  A  dom  ( { j }  X.  B
)
228226, 227syl6sseq 3535 . . . . . . . . . . . . 13  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  C_  U_ j  e.  A  dom  ( { j }  X.  B
) )
229 dmxpss 5423 . . . . . . . . . . . . . . . . 17  |-  dom  ( { j }  X.  B )  C_  { j }
230229a1i 11 . . . . . . . . . . . . . . . 16  |-  ( j  e.  A  ->  dom  ( { j }  X.  B )  C_  { j } )
231 snssi 4160 . . . . . . . . . . . . . . . 16  |-  ( j  e.  A  ->  { j }  C_  A )
232230, 231sstrd 3499 . . . . . . . . . . . . . . 15  |-  ( j  e.  A  ->  dom  ( { j }  X.  B )  C_  A
)
233232rgen 2814 . . . . . . . . . . . . . 14  |-  A. j  e.  A  dom  ( { j }  X.  B
)  C_  A
234 iunss 4356 . . . . . . . . . . . . . 14  |-  ( U_ j  e.  A  dom  ( { j }  X.  B )  C_  A  <->  A. j  e.  A  dom  ( { j }  X.  B )  C_  A
)
235233, 234mpbir 209 . . . . . . . . . . . . 13  |-  U_ j  e.  A  dom  ( { j }  X.  B
)  C_  A
236228, 235syl6ss 3501 . . . . . . . . . . . 12  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  C_  A )
23718dmex 6706 . . . . . . . . . . . . 13  |-  dom  c  e.  _V
238237elpw 4005 . . . . . . . . . . . 12  |-  ( dom  c  e.  ~P A  <->  dom  c  C_  A )
239236, 238sylibr 212 . . . . . . . . . . 11  |-  ( c 
C_  U_ j  e.  A  ( { j }  X.  B )  ->  dom  c  e.  ~P A
)
240224, 225, 2393syl 20 . . . . . . . . . 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 27618 . . . . . . . . . . 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 7795 . . . . . . . . . . 11  |-  ( c  e.  Fin  ->  dom  c  e.  Fin )
243241, 242syl 16 . . . . . . . . . 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 3674 . . . . . . . . 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 6298 . . . . . . . . . 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 4519 . . . . . . . . . . 11  |-  ( a  =  dom  c  -> 
( j  e.  a 
|-> Σ* k  e.  B C
)  =  ( j  e.  dom  c  |-> Σ* k  e.  B C ) )
248247oveq2d 6286 . . . . . . . . . 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 5239 . . . . . . . . 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 659 . . . . . . . 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 459 . . . . . . . . 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 4451 . . . . . . . 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 758 . . . . . . . . 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 2616 . . . . . . . . . . . . . . . 16  |-  F/_ z
( RR*ss  ( 0 [,] +oo ) )
256 nfcv 2616 . . . . . . . . . . . . . . . 16  |-  F/_ z  gsumg
257 nfmpt1 4528 . . . . . . . . . . . . . . . 16  |-  F/_ z
( z  e.  c 
|->  F )
258255, 256, 257nfov 6296 . . . . . . . . . . . . . . 15  |-  F/_ z
( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( z  e.  c 
|->  F ) )
259110, 111, 258nfbr 4483 . . . . . . . . . . . . . 14  |-  F/ z  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) )
260109, 259nfan 1933 . . . . . . . . . . . . 13  |-  F/ z ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
261 nfv 1712 . . . . . . . . . . . . 13  |-  F/ z  c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )
262260, 261nfan 1933 . . . . . . . . . . . 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 765 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . 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 3489 . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . 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 432 . . . . . . . . . . . 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 2854 . . . . . . . . . . 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 17190 . . . . . . . . . 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 3487 . . . . . . . . 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 1712 . . . . . . . . . . . . 13  |-  F/ j ( ( ph  /\  s  e.  RR* )  /\  s  <  ( ( RR*ss  ( 0 [,] +oo ) )  gsumg  ( z  e.  c 
|->  F ) ) )
272 nfcv 2616 . . . . . . . . . . . . . 14  |-  F/_ j
c
27325nfpw 4011 . . . . . . . . . . . . . . 15  |-  F/_ j ~P U_ j  e.  A  ( { j }  X.  B )
274 nfcv 2616 . . . . . . . . . . . . . . 15  |-  F/_ j Fin
275273, 274nfin 3691 . . . . . . . . . . . . . 14  |-  F/_ j
( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
276272, 275nfel 2629 . . . . . . . . . . . . 13  |-  F/ j  c  e.  ( ~P
U_ j  e.  A  ( { j }  X.  B )  i^i  Fin )
277271, 276nfan 1933 . . . . . . . . . . . 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 751 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  ( ~P U_ j  e.  A  ( {
j }  X.  B
)  i^i  Fin )
)  /\  j  e.  dom  c )  ->  ph )
27979, 236syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  ( ~P U_ j  e.  A  ( { j }  X.  B )  i^i  Fin ) )  ->  dom  c  C_  A )
280279sselda 3489 . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . 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 716 . . . . . . . . . . . . . 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 716 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  s  e.  RR* )  /\  s  <  ( (
RR*ss  ( 0 [,] +oo ) )  gsumg