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 snex
 |-  { 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 )