Metamath Proof Explorer

Theorem esumiun

Description: Sum over a nonnecessarily disjoint indexed union. The inequality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019)

Ref Expression
Hypotheses esumiun.0 
|- ( ph -> A e. V )
esumiun.1 
|- ( ( ph /\ j e. A ) -> B e. W )
esumiun.2 
|- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
Assertion esumiun 
|- ( ph -> sum* k e. U_ j e. A B C <_ sum* j e. A sum* k e. B C )

Proof

Step Hyp Ref Expression
1 esumiun.0 
 |-  ( ph -> A e. V )
2 esumiun.1 
 |-  ( ( ph /\ j e. A ) -> B e. W )
3 esumiun.2 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
4 1 2 aciunf1 
 |-  ( ph -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) )
5 f1f1orn 
 |-  ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) -> f : U_ j e. A B -1-1-onto-> ran f )
6 5 anim1i 
 |-  ( ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) )
7 f1f 
 |-  ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) -> f : U_ j e. A B --> U_ j e. A ( { j } X. B ) )
8 7 frnd 
 |-  ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) -> ran f C_ U_ j e. A ( { j } X. B ) )
9 8 adantr 
 |-  ( ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ran f C_ U_ j e. A ( { j } X. B ) )
10 6 9 jca 
 |-  ( ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) )
11 10 eximi 
 |-  ( E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> E. f ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) )
12 4 11 syl 
 |-  ( ph -> E. f ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) )
13 nfv 
 |-  F/ z ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) )
14 nfcv 
 |-  F/_ z C
15 nfcsb1v 
 |-  F/_ k [_ ( 2nd ` z ) / k ]_ C
16 nfcv 
 |-  F/_ z U_ j e. A B
17 nfcv 
 |-  F/_ z ran f
18 nfcv 
 |-  F/_ z `' f
19 csbeq1a 
 |-  ( k = ( 2nd ` z ) -> C = [_ ( 2nd ` z ) / k ]_ C )
20 2 ralrimiva 
 |-  ( ph -> A. j e. A B e. W )
21 iunexg 
 |-  ( ( A e. V /\ A. j e. A B e. W ) -> U_ j e. A B e. _V )
22 1 20 21 syl2anc 
 |-  ( ph -> U_ j e. A B e. _V )
23 22 adantr 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> U_ j e. A B e. _V )
24 simprl 
 |-  ( ( ph /\ ( f : U_ j e. A B -1-1-onto-> ran f /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> f : U_ j e. A B -1-1-onto-> ran f )
25 f1ocnv 
 |-  ( f : U_ j e. A B -1-1-onto-> ran f -> `' f : ran f -1-1-onto-> U_ j e. A B )
26 24 25 syl 
 |-  ( ( ph /\ ( f : U_ j e. A B -1-1-onto-> ran f /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ j e. A B )
27 26 adantrlr 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ j e. A B )
28 nfv 
 |-  F/ j ph
29 nfcv 
 |-  F/_ j f
30 nfiu1 
 |-  F/_ j U_ j e. A B
31 29 nfrn 
 |-  F/_ j ran f
32 29 30 31 nff1o 
 |-  F/ j f : U_ j e. A B -1-1-onto-> ran f
33 nfv 
 |-  F/ j ( 2nd ` ( f ` l ) ) = l
34 30 33 nfralw 
 |-  F/ j A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l
35 32 34 nfan 
 |-  F/ j ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l )
36 nfcv 
 |-  F/_ j ran f
37 nfiu1 
 |-  F/_ j U_ j e. A ( { j } X. B )
38 36 37 nfss 
 |-  F/ j ran f C_ U_ j e. A ( { j } X. B )
39 35 38 nfan 
 |-  F/ j ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) )
40 28 39 nfan 
 |-  F/ j ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) )
41 nfv 
 |-  F/ j z e. ran f
42 40 41 nfan 
 |-  F/ j ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f )
43 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( f ` k ) = z )
44 43 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = ( 2nd ` z ) )
45 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> k e. U_ j e. A B )
46 simp-4r 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) )
47 46 simpld 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) )
48 47 simprd 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l )
49 48 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l )
50 2fveq3 
 |-  ( l = k -> ( 2nd ` ( f ` l ) ) = ( 2nd ` ( f ` k ) ) )
51 id 
 |-  ( l = k -> l = k )
52 50 51 eqeq12d 
 |-  ( l = k -> ( ( 2nd ` ( f ` l ) ) = l <-> ( 2nd ` ( f ` k ) ) = k ) )
53 52 rspcva 
 |-  ( ( k e. U_ j e. A B /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( 2nd ` ( f ` k ) ) = k )
54 45 49 53 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = k )
55 44 54 eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` z ) = k )
56 47 simpld 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> f : U_ j e. A B -1-1-onto-> ran f )
57 56 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> f : U_ j e. A B -1-1-onto-> ran f )
58 f1ocnvfv1 
 |-  ( ( f : U_ j e. A B -1-1-onto-> ran f /\ k e. U_ j e. A B ) -> ( `' f ` ( f ` k ) ) = k )
59 57 45 58 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = k )
60 43 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = ( `' f ` z ) )
61 55 59 60 3eqtr2rd 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` z ) = ( 2nd ` z ) )
62 f1ofn 
 |-  ( f : U_ j e. A B -1-1-onto-> ran f -> f Fn U_ j e. A B )
63 56 62 syl 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> f Fn U_ j e. A B )
64 simpllr 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> z e. ran f )
65 fvelrnb 
 |-  ( f Fn U_ j e. A B -> ( z e. ran f <-> E. k e. U_ j e. A B ( f ` k ) = z ) )
66 65 biimpa 
 |-  ( ( f Fn U_ j e. A B /\ z e. ran f ) -> E. k e. U_ j e. A B ( f ` k ) = z )
67 63 64 66 syl2anc 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E. k e. U_ j e. A B ( f ` k ) = z )
68 61 67 r19.29a 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( `' f ` z ) = ( 2nd ` z ) )
69 simprr 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> ran f C_ U_ j e. A ( { j } X. B ) )
70 69 sselda 
 |-  ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) -> z e. U_ j e. A ( { j } X. B ) )
71 eliun 
 |-  ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) )
72 70 71 sylib 
 |-  ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) -> E. j e. A z e. ( { j } X. B ) )
73 42 68 72 r19.29af 
 |-  ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) -> ( `' f ` z ) = ( 2nd ` z ) )
74 nfcv 
 |-  F/_ j k
75 74 30 nfel 
 |-  F/ j k e. U_ j e. A B
76 28 75 nfan 
 |-  F/ j ( ph /\ k e. U_ j e. A B )
77 3 adantllr 
 |-  ( ( ( ( ph /\ k e. U_ j e. A B ) /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
78 eliun 
 |-  ( k e. U_ j e. A B <-> E. j e. A k e. B )
79 78 bilani 
 |-  ( ( ph /\ k e. U_ j e. A B ) -> E. j e. A k e. B )
80 76 77 79 r19.29af 
 |-  ( ( ph /\ k e. U_ j e. A B ) -> C e. ( 0 [,] +oo ) )
81 80 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ k e. U_ j e. A B ) -> C e. ( 0 [,] +oo ) )
82 13 14 15 16 17 18 19 23 27 73 81 esumf1o 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* k e. U_ j e. A B C = sum* z e. ran f [_ ( 2nd ` z ) / k ]_ C )
83 82 eqcomd 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* z e. ran f [_ ( 2nd ` z ) / k ]_ C = sum* k e. U_ j e. A B C )
84 vsnex 
 |-  { j } e. _V
85 84 a1i 
 |-  ( ( ph /\ j e. A ) -> { j } e. _V )
86 85 2 xpexd 
 |-  ( ( ph /\ j e. A ) -> ( { j } X. B ) e. _V )
87 86 ralrimiva 
 |-  ( ph -> A. j e. A ( { j } X. B ) e. _V )
88 iunexg 
 |-  ( ( A e. V /\ A. j e. A ( { j } X. B ) e. _V ) -> U_ j e. A ( { j } X. B ) e. _V )
89 1 87 88 syl2anc 
 |-  ( ph -> U_ j e. A ( { j } X. B ) e. _V )
90 89 adantr 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> U_ j e. A ( { j } X. B ) e. _V )
91 nfcv 
 |-  F/_ j z
92 91 37 nfel 
 |-  F/ j z e. U_ j e. A ( { j } X. B )
93 28 92 nfan 
 |-  F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) )
94 nfcv 
 |-  F/_ j ( 2nd ` z )
95 nfcv 
 |-  F/_ j C
96 94 95 nfcsbw 
 |-  F/_ j [_ ( 2nd ` z ) / k ]_ C
97 nfcv 
 |-  F/_ j ( 0 [,] +oo )
98 96 97 nfel 
 |-  F/ j [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo )
99 simprr 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> ( 2nd ` z ) e. B )
100 simplll 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> ph )
101 simplr 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> j e. A )
102 3 ralrimiva 
 |-  ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
103 100 101 102 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> A. k e. B C e. ( 0 [,] +oo ) )
104 rspcsbela 
 |-  ( ( ( 2nd ` z ) e. B /\ A. k e. B C e. ( 0 [,] +oo ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) )
105 99 103 104 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) )
106 xp1st 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
107 elsni 
 |-  ( ( 1st ` z ) e. { j } -> ( 1st ` z ) = j )
108 106 107 syl 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
109 xp2nd 
 |-  ( z e. ( { j } X. B ) -> ( 2nd ` z ) e. B )
110 108 109 jca 
 |-  ( z e. ( { j } X. B ) -> ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
111 110 reximi 
 |-  ( E. j e. A z e. ( { j } X. B ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
112 71 111 sylbi 
 |-  ( z e. U_ j e. A ( { j } X. B ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
113 112 adantl 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
114 93 98 105 113 r19.29af2 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) )
115 114 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. U_ j e. A ( { j } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) )
116 simprr 
 |-  ( ( ph /\ ( f : U_ j e. A B -1-1-onto-> ran f /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> ran f C_ U_ j e. A ( { j } X. B ) )
117 116 adantrlr 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> ran f C_ U_ j e. A ( { j } X. B ) )
118 13 90 115 117 esummono 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* z e. ran f [_ ( 2nd ` z ) / k ]_ C <_ sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C )
119 83 118 eqbrtrrd 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* k e. U_ j e. A B C <_ sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C )
120 vex 
 |-  j e. _V
121 vex 
 |-  k e. _V
122 120 121 op2ndd 
 |-  ( z = <. j , k >. -> ( 2nd ` z ) = k )
123 122 eqcomd 
 |-  ( z = <. j , k >. -> k = ( 2nd ` z ) )
124 123 19 syl 
 |-  ( z = <. j , k >. -> C = [_ ( 2nd ` z ) / k ]_ C )
125 124 eqcomd 
 |-  ( z = <. j , k >. -> [_ ( 2nd ` z ) / k ]_ C = C )
126 3 anasss 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
127 15 125 1 2 126 esum2d 
 |-  ( ph -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C )
128 127 adantr 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C )
129 119 128 breqtrrd 
 |-  ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* k e. U_ j e. A B C <_ sum* j e. A sum* k e. B C )
130 12 129 exlimddv 
 |-  ( ph -> sum* k e. U_ j e. A B C <_ sum* j e. A sum* k e. B C )