Metamath Proof Explorer

Theorem fsumiunle

Description: Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021)

Ref Expression
Hypotheses fsumiunle.1 
|- ( ph -> A e. Fin )
fsumiunle.2 
|- ( ( ph /\ x e. A ) -> B e. Fin )
fsumiunle.3 
|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. RR )
fsumiunle.4 
|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> 0 <_ C )
Assertion fsumiunle 
|- ( ph -> sum_ k e. U_ x e. A B C <_ sum_ x e. A sum_ k e. B C )

Proof

Step Hyp Ref Expression
1 fsumiunle.1 
 |-  ( ph -> A e. Fin )
2 fsumiunle.2 
 |-  ( ( ph /\ x e. A ) -> B e. Fin )
3 fsumiunle.3 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. RR )
4 fsumiunle.4 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> 0 <_ C )
5 1 2 aciunf1 
 |-  ( ph -> E. f ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) )
6 f1f1orn 
 |-  ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) -> f : U_ x e. A B -1-1-onto-> ran f )
7 6 anim1i 
 |-  ( ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) )
8 f1f 
 |-  ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) -> f : U_ x e. A B --> U_ x e. A ( { x } X. B ) )
9 8 frnd 
 |-  ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) -> ran f C_ U_ x e. A ( { x } X. B ) )
10 9 adantr 
 |-  ( ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ran f C_ U_ x e. A ( { x } X. B ) )
11 7 10 jca 
 |-  ( ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
12 11 eximi 
 |-  ( E. f ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> E. f ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
13 5 12 syl 
 |-  ( ph -> E. f ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
14 csbeq1a 
 |-  ( k = y -> C = [_ y / k ]_ C )
15 nfcv 
 |-  F/_ y C
16 nfcsb1v 
 |-  F/_ k [_ y / k ]_ C
17 14 15 16 cbvsum 
 |-  sum_ k e. U_ x e. A B C = sum_ y e. U_ x e. A B [_ y / k ]_ C
18 csbeq1 
 |-  ( y = ( 2nd ` z ) -> [_ y / k ]_ C = [_ ( 2nd ` z ) / k ]_ C )
19 snfi 
 |-  { x } e. Fin
20 xpfi 
 |-  ( ( { x } e. Fin /\ B e. Fin ) -> ( { x } X. B ) e. Fin )
21 19 2 20 sylancr 
 |-  ( ( ph /\ x e. A ) -> ( { x } X. B ) e. Fin )
22 21 ralrimiva 
 |-  ( ph -> A. x e. A ( { x } X. B ) e. Fin )
23 iunfi 
 |-  ( ( A e. Fin /\ A. x e. A ( { x } X. B ) e. Fin ) -> U_ x e. A ( { x } X. B ) e. Fin )
24 1 22 23 syl2anc 
 |-  ( ph -> U_ x e. A ( { x } X. B ) e. Fin )
25 24 adantr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> U_ x e. A ( { x } X. B ) e. Fin )
26 simprr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> ran f C_ U_ x e. A ( { x } X. B ) )
27 25 26 ssfid 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> ran f e. Fin )
28 simprl 
 |-  ( ( ph /\ ( f : U_ x e. A B -1-1-onto-> ran f /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> f : U_ x e. A B -1-1-onto-> ran f )
29 f1ocnv 
 |-  ( f : U_ x e. A B -1-1-onto-> ran f -> `' f : ran f -1-1-onto-> U_ x e. A B )
30 28 29 syl 
 |-  ( ( ph /\ ( f : U_ x e. A B -1-1-onto-> ran f /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ x e. A B )
31 30 adantrlr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ x e. A B )
32 nfv 
 |-  F/ x ph
33 nfcv 
 |-  F/_ x f
34 nfiu1 
 |-  F/_ x U_ x e. A B
35 33 nfrn 
 |-  F/_ x ran f
36 33 34 35 nff1o 
 |-  F/ x f : U_ x e. A B -1-1-onto-> ran f
37 nfv 
 |-  F/ x ( 2nd ` ( f ` l ) ) = l
38 34 37 nfralw 
 |-  F/ x A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l
39 36 38 nfan 
 |-  F/ x ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l )
40 nfcv 
 |-  F/_ x ran f
41 nfiu1 
 |-  F/_ x U_ x e. A ( { x } X. B )
42 40 41 nfss 
 |-  F/ x ran f C_ U_ x e. A ( { x } X. B )
43 39 42 nfan 
 |-  F/ x ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) )
44 32 43 nfan 
 |-  F/ x ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
45 nfv 
 |-  F/ x z e. ran f
46 44 45 nfan 
 |-  F/ x ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f )
47 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( f ` k ) = z )
48 47 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = ( 2nd ` z ) )
49 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> k e. U_ x e. A B )
50 simp-4r 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
51 50 simpld 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) )
52 51 simprd 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l )
53 52 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l )
54 2fveq3 
 |-  ( l = k -> ( 2nd ` ( f ` l ) ) = ( 2nd ` ( f ` k ) ) )
55 id 
 |-  ( l = k -> l = k )
56 54 55 eqeq12d 
 |-  ( l = k -> ( ( 2nd ` ( f ` l ) ) = l <-> ( 2nd ` ( f ` k ) ) = k ) )
57 56 rspcva 
 |-  ( ( k e. U_ x e. A B /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( 2nd ` ( f ` k ) ) = k )
58 49 53 57 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = k )
59 48 58 eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` z ) = k )
60 51 simpld 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> f : U_ x e. A B -1-1-onto-> ran f )
61 60 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> f : U_ x e. A B -1-1-onto-> ran f )
62 f1ocnvfv1 
 |-  ( ( f : U_ x e. A B -1-1-onto-> ran f /\ k e. U_ x e. A B ) -> ( `' f ` ( f ` k ) ) = k )
63 61 49 62 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = k )
64 47 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = ( `' f ` z ) )
65 59 63 64 3eqtr2rd 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` z ) = ( 2nd ` z ) )
66 f1ofn 
 |-  ( f : U_ x e. A B -1-1-onto-> ran f -> f Fn U_ x e. A B )
67 60 66 syl 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> f Fn U_ x e. A B )
68 simpllr 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> z e. ran f )
69 fvelrnb 
 |-  ( f Fn U_ x e. A B -> ( z e. ran f <-> E. k e. U_ x e. A B ( f ` k ) = z ) )
70 69 biimpa 
 |-  ( ( f Fn U_ x e. A B /\ z e. ran f ) -> E. k e. U_ x e. A B ( f ` k ) = z )
71 67 68 70 syl2anc 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> E. k e. U_ x e. A B ( f ` k ) = z )
72 65 71 r19.29a 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( `' f ` z ) = ( 2nd ` z ) )
73 26 sselda 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) -> z e. U_ x e. A ( { x } X. B ) )
74 eliun 
 |-  ( z e. U_ x e. A ( { x } X. B ) <-> E. x e. A z e. ( { x } X. B ) )
75 73 74 sylib 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) -> E. x e. A z e. ( { x } X. B ) )
76 46 72 75 r19.29af 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) -> ( `' f ` z ) = ( 2nd ` z ) )
77 nfv 
 |-  F/ k ( ph /\ y e. U_ x e. A B )
78 nfcv 
 |-  F/_ k CC
79 16 78 nfel 
 |-  F/ k [_ y / k ]_ C e. CC
80 77 79 nfim 
 |-  F/ k ( ( ph /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC )
81 eleq1w 
 |-  ( k = y -> ( k e. U_ x e. A B <-> y e. U_ x e. A B ) )
82 81 anbi2d 
 |-  ( k = y -> ( ( ph /\ k e. U_ x e. A B ) <-> ( ph /\ y e. U_ x e. A B ) ) )
83 14 eleq1d 
 |-  ( k = y -> ( C e. CC <-> [_ y / k ]_ C e. CC ) )
84 82 83 imbi12d 
 |-  ( k = y -> ( ( ( ph /\ k e. U_ x e. A B ) -> C e. CC ) <-> ( ( ph /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC ) ) )
85 nfcv 
 |-  F/_ x k
86 85 34 nfel 
 |-  F/ x k e. U_ x e. A B
87 32 86 nfan 
 |-  F/ x ( ph /\ k e. U_ x e. A B )
88 3 adantllr 
 |-  ( ( ( ( ph /\ k e. U_ x e. A B ) /\ x e. A ) /\ k e. B ) -> C e. RR )
89 88 recnd 
 |-  ( ( ( ( ph /\ k e. U_ x e. A B ) /\ x e. A ) /\ k e. B ) -> C e. CC )
90 eliun 
 |-  ( k e. U_ x e. A B <-> E. x e. A k e. B )
91 90 biimpi 
 |-  ( k e. U_ x e. A B -> E. x e. A k e. B )
92 91 adantl 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> E. x e. A k e. B )
93 87 89 92 r19.29af 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> C e. CC )
94 80 84 93 chvarfv 
 |-  ( ( ph /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC )
95 94 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC )
96 18 27 31 76 95 fsumf1o 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ y e. U_ x e. A B [_ y / k ]_ C = sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C )
97 17 96 eqtrid 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ k e. U_ x e. A B C = sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C )
98 97 eqcomd 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C = sum_ k e. U_ x e. A B C )
99 nfcv 
 |-  F/_ x z
100 99 41 nfel 
 |-  F/ x z e. U_ x e. A ( { x } X. B )
101 32 100 nfan 
 |-  F/ x ( ph /\ z e. U_ x e. A ( { x } X. B ) )
102 xp2nd 
 |-  ( z e. ( { x } X. B ) -> ( 2nd ` z ) e. B )
103 102 adantl 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( 2nd ` z ) e. B )
104 3 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. k e. B C e. RR )
105 104 adantlr 
 |-  ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) -> A. k e. B C e. RR )
106 105 adantr 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> A. k e. B C e. RR )
107 nfcsb1v 
 |-  F/_ k [_ ( 2nd ` z ) / k ]_ C
108 107 nfel1 
 |-  F/ k [_ ( 2nd ` z ) / k ]_ C e. RR
109 csbeq1a 
 |-  ( k = ( 2nd ` z ) -> C = [_ ( 2nd ` z ) / k ]_ C )
110 109 eleq1d 
 |-  ( k = ( 2nd ` z ) -> ( C e. RR <-> [_ ( 2nd ` z ) / k ]_ C e. RR ) )
111 108 110 rspc 
 |-  ( ( 2nd ` z ) e. B -> ( A. k e. B C e. RR -> [_ ( 2nd ` z ) / k ]_ C e. RR ) )
112 111 imp 
 |-  ( ( ( 2nd ` z ) e. B /\ A. k e. B C e. RR ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
113 103 106 112 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
114 74 biimpi 
 |-  ( z e. U_ x e. A ( { x } X. B ) -> E. x e. A z e. ( { x } X. B ) )
115 114 adantl 
 |-  ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) -> E. x e. A z e. ( { x } X. B ) )
116 101 113 115 r19.29af 
 |-  ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
117 116 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. U_ x e. A ( { x } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
118 xp1st 
 |-  ( z e. ( { x } X. B ) -> ( 1st ` z ) e. { x } )
119 elsni 
 |-  ( ( 1st ` z ) e. { x } -> ( 1st ` z ) = x )
120 118 119 syl 
 |-  ( z e. ( { x } X. B ) -> ( 1st ` z ) = x )
121 120 102 jca 
 |-  ( z e. ( { x } X. B ) -> ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) )
122 simplll 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) ) -> ph )
123 simplr 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) ) -> x e. A )
124 4 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. k e. B 0 <_ C )
125 122 123 124 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) ) -> A. k e. B 0 <_ C )
126 121 125 sylan2 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> A. k e. B 0 <_ C )
127 nfcv 
 |-  F/_ k 0
128 nfcv 
 |-  F/_ k <_
129 127 128 107 nfbr 
 |-  F/ k 0 <_ [_ ( 2nd ` z ) / k ]_ C
130 109 breq2d 
 |-  ( k = ( 2nd ` z ) -> ( 0 <_ C <-> 0 <_ [_ ( 2nd ` z ) / k ]_ C ) )
131 129 130 rspc 
 |-  ( ( 2nd ` z ) e. B -> ( A. k e. B 0 <_ C -> 0 <_ [_ ( 2nd ` z ) / k ]_ C ) )
132 131 imp 
 |-  ( ( ( 2nd ` z ) e. B /\ A. k e. B 0 <_ C ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
133 103 126 132 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
134 101 133 115 r19.29af 
 |-  ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
135 134 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. U_ x e. A ( { x } X. B ) ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
136 25 117 135 26 fsumless 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C <_ sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
137 98 136 eqbrtrrd 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ k e. U_ x e. A B C <_ sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
138 14 15 16 cbvsum 
 |-  sum_ k e. B C = sum_ y e. B [_ y / k ]_ C
139 138 a1i 
 |-  ( ph -> sum_ k e. B C = sum_ y e. B [_ y / k ]_ C )
140 139 sumeq2sdv 
 |-  ( ph -> sum_ x e. A sum_ k e. B C = sum_ x e. A sum_ y e. B [_ y / k ]_ C )
141 vex 
 |-  x e. _V
142 vex 
 |-  y e. _V
143 141 142 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
144 143 eqcomd 
 |-  ( z = <. x , y >. -> y = ( 2nd ` z ) )
145 144 csbeq1d 
 |-  ( z = <. x , y >. -> [_ y / k ]_ C = [_ ( 2nd ` z ) / k ]_ C )
146 145 eqcomd 
 |-  ( z = <. x , y >. -> [_ ( 2nd ` z ) / k ]_ C = [_ y / k ]_ C )
147 nfv 
 |-  F/ k ( ( ph /\ x e. A ) /\ y e. B )
148 16 nfel1 
 |-  F/ k [_ y / k ]_ C e. CC
149 147 148 nfim 
 |-  F/ k ( ( ( ph /\ x e. A ) /\ y e. B ) -> [_ y / k ]_ C e. CC )
150 eleq1w 
 |-  ( k = y -> ( k e. B <-> y e. B ) )
151 150 anbi2d 
 |-  ( k = y -> ( ( ( ph /\ x e. A ) /\ k e. B ) <-> ( ( ph /\ x e. A ) /\ y e. B ) ) )
152 151 83 imbi12d 
 |-  ( k = y -> ( ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC ) <-> ( ( ( ph /\ x e. A ) /\ y e. B ) -> [_ y / k ]_ C e. CC ) ) )
153 3 recnd 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC )
154 149 152 153 chvarfv 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> [_ y / k ]_ C e. CC )
155 154 anasss 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> [_ y / k ]_ C e. CC )
156 146 1 2 155 fsum2d 
 |-  ( ph -> sum_ x e. A sum_ y e. B [_ y / k ]_ C = sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
157 140 156 eqtrd 
 |-  ( ph -> sum_ x e. A sum_ k e. B C = sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
158 157 adantr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ x e. A sum_ k e. B C = sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
159 137 158 breqtrrd 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ k e. U_ x e. A B C <_ sum_ x e. A sum_ k e. B C )
160 13 159 exlimddv 
 |-  ( ph -> sum_ k e. U_ x e. A B C <_ sum_ x e. A sum_ k e. B C )