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 biimpi 
 |-  ( k e. U_ j e. A B -> E. j e. A k e. B )
80 79 adantl 
 |-  ( ( ph /\ k e. U_ j e. A B ) -> E. j e. A k e. B )
81 76 77 80 r19.29af 
 |-  ( ( ph /\ k e. U_ j e. A B ) -> C e. ( 0 [,] +oo ) )
82 81 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 ) )
83 13 14 15 16 17 18 19 23 27 73 82 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 )
84 83 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 )
85 vsnex 
 |-  { j } e. _V
86 85 a1i 
 |-  ( ( ph /\ j e. A ) -> { j } e. _V )
87 86 2 xpexd 
 |-  ( ( ph /\ j e. A ) -> ( { j } X. B ) e. _V )
88 87 ralrimiva 
 |-  ( ph -> A. j e. A ( { j } X. B ) e. _V )
89 iunexg 
 |-  ( ( A e. V /\ A. j e. A ( { j } X. B ) e. _V ) -> U_ j e. A ( { j } X. B ) e. _V )
90 1 88 89 syl2anc 
 |-  ( ph -> U_ j e. A ( { j } X. B ) e. _V )
91 90 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 )
92 nfcv 
 |-  F/_ j z
93 92 37 nfel 
 |-  F/ j z e. U_ j e. A ( { j } X. B )
94 28 93 nfan 
 |-  F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) )
95 nfcv 
 |-  F/_ j ( 2nd ` z )
96 nfcv 
 |-  F/_ j C
97 95 96 nfcsbw 
 |-  F/_ j [_ ( 2nd ` z ) / k ]_ C
98 nfcv 
 |-  F/_ j ( 0 [,] +oo )
99 97 98 nfel 
 |-  F/ j [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo )
100 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 )
101 simplll 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> ph )
102 simplr 
 |-  ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> j e. A )
103 3 ralrimiva 
 |-  ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) )
104 101 102 103 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 ) )
105 rspcsbela 
 |-  ( ( ( 2nd ` z ) e. B /\ A. k e. B C e. ( 0 [,] +oo ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) )
106 100 104 105 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 ) )
107 xp1st 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
108 elsni 
 |-  ( ( 1st ` z ) e. { j } -> ( 1st ` z ) = j )
109 107 108 syl 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
110 xp2nd 
 |-  ( z e. ( { j } X. B ) -> ( 2nd ` z ) e. B )
111 109 110 jca 
 |-  ( z e. ( { j } X. B ) -> ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
112 111 reximi 
 |-  ( E. j e. A z e. ( { j } X. B ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
113 71 112 sylbi 
 |-  ( z e. U_ j e. A ( { j } X. B ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
114 113 adantl 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) )
115 94 99 106 114 r19.29af2 
 |-  ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) )
116 115 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 ) )
117 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 ) )
118 117 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 ) )
119 13 91 116 118 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 )
120 84 119 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 )
121 vex 
 |-  j e. _V
122 vex 
 |-  k e. _V
123 121 122 op2ndd 
 |-  ( z = <. j , k >. -> ( 2nd ` z ) = k )
124 123 eqcomd 
 |-  ( z = <. j , k >. -> k = ( 2nd ` z ) )
125 124 19 syl 
 |-  ( z = <. j , k >. -> C = [_ ( 2nd ` z ) / k ]_ C )
126 125 eqcomd 
 |-  ( z = <. j , k >. -> [_ ( 2nd ` z ) / k ]_ C = C )
127 3 anasss 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) )
128 15 126 1 2 127 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 )
129 128 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 )
130 120 129 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 )
131 12 130 exlimddv 
 |-  ( ph -> sum* k e. U_ j e. A B C <_ sum* j e. A sum* k e. B C )