Theorem sge0iunmptlemre

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0iunmptlemre.a	|- ( ph -> A e. V )
	sge0iunmptlemre.b	|- ( ( ph /\ x e. A ) -> B e. W )
	sge0iunmptlemre.dj	|- ( ph -> Disj_ x e. A B )
	sge0iunmptlemre.c	|- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )
	sge0iunmptlemre.re	|- ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR )
	sge0iunmptlemre.sxr	|- ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) e. RR* )
	sge0iunmptlemre.ssxr	|- ( ph -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) e. RR* )
	sge0iunmptlemre.f	|- ( ph -> ( k e. U_ x e. A B |-> C ) : U_ x e. A B --> ( 0 [,] +oo ) )
	sge0iunmptlemre.iue	|- ( ph -> U_ x e. A B e. _V )
Assertion	sge0iunmptlemre	|- ( 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		sge0iunmptlemre.a	|- ( ph -> A e. V )
2		sge0iunmptlemre.b	|- ( ( ph /\ x e. A ) -> B e. W )
3		sge0iunmptlemre.dj	|- ( ph -> Disj_ x e. A B )
4		sge0iunmptlemre.c	|- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )
5		sge0iunmptlemre.re	|- ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR )
6		sge0iunmptlemre.sxr	|- ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) e. RR* )
7		sge0iunmptlemre.ssxr	|- ( ph -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) e. RR* )
8		sge0iunmptlemre.f	|- ( ph -> ( k e. U_ x e. A B |-> C ) : U_ x e. A B --> ( 0 [,] +oo ) )
9		sge0iunmptlemre.iue	|- ( ph -> U_ x e. A B e. _V )
10		elpwinss	|- ( y e. ( ~P U_ x e. A B i^i Fin ) -> y C_ U_ x e. A B )
11	10	resmptd	|- ( y e. ( ~P U_ x e. A B i^i Fin ) -> ( ( k e. U_ x e. A B |-> C ) |` y ) = ( k e. y |-> C ) )
12	11	fveq2d	|- ( y e. ( ~P U_ x e. A B i^i Fin ) -> ( sum^ ` ( ( k e. U_ x e. A B |-> C ) |` y ) ) = ( sum^ ` ( k e. y |-> C ) ) )
13	12	adantl	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( ( k e. U_ x e. A B |-> C ) |` y ) ) = ( sum^ ` ( k e. y |-> C ) ) )
14		elinel2	|- ( y e. ( ~P U_ x e. A B i^i Fin ) -> y e. Fin )
15	14	adantl	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> y e. Fin )
16	10	sselda	|- ( ( y e. ( ~P U_ x e. A B i^i Fin ) /\ k e. y ) -> k e. U_ x e. A B )
17		eliun	|- ( k e. U_ x e. A B <-> E. x e. A k e. B )
18	16 17	sylib	|- ( ( y e. ( ~P U_ x e. A B i^i Fin ) /\ k e. y ) -> E. x e. A k e. B )
19	18	adantll	|- ( ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) /\ k e. y ) -> E. x e. A k e. B )
20		nfv	|- F/ x ph
21		nfcv	|- F/_ x y
22		nfiu1	|- F/_ x U_ x e. A B
23	22	nfpw	|- F/_ x ~P U_ x e. A B
24		nfcv	|- F/_ x Fin
25	23 24	nfin	|- F/_ x ( ~P U_ x e. A B i^i Fin )
26	21 25	nfel	|- F/ x y e. ( ~P U_ x e. A B i^i Fin )
27	20 26	nfan	|- F/ x ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) )
28		nfv	|- F/ x k e. y
29	27 28	nfan	|- F/ x ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) /\ k e. y )
30		nfv	|- F/ x C e. ( 0 [,) +oo )
31		simp3	|- ( ( ph /\ x e. A /\ k e. B ) -> k e. B )
32		eqid	|- ( k e. B |-> C ) = ( k e. B |-> C )
33	32	fvmpt2	|- ( ( k e. B /\ C e. ( 0 [,] +oo ) ) -> ( ( k e. B |-> C ) ` k ) = C )
34	31 4 33	syl2anc	|- ( ( ph /\ x e. A /\ k e. B ) -> ( ( k e. B |-> C ) ` k ) = C )
35	34	eqcomd	|- ( ( ph /\ x e. A /\ k e. B ) -> C = ( ( k e. B |-> C ) ` k ) )
36	4	3expa	|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) )
37	36 32	fmptd	|- ( ( ph /\ x e. A ) -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) )
38	37	3adant3	|- ( ( ph /\ x e. A /\ k e. B ) -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) )
39	2	3adant3	|- ( ( ph /\ x e. A /\ k e. B ) -> B e. W )
40	5	3adant3	|- ( ( ph /\ x e. A /\ k e. B ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR )
41	39 38 40	sge0rern	|- ( ( ph /\ x e. A /\ k e. B ) -> -. +oo e. ran ( k e. B |-> C ) )
42	38 41	fge0iccico	|- ( ( ph /\ x e. A /\ k e. B ) -> ( k e. B |-> C ) : B --> ( 0 [,) +oo ) )
43	42 31	ffvelrnd	|- ( ( ph /\ x e. A /\ k e. B ) -> ( ( k e. B |-> C ) ` k ) e. ( 0 [,) +oo ) )
44	35 43	eqeltrd	|- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,) +oo ) )
45	44	3exp	|- ( ph -> ( x e. A -> ( k e. B -> C e. ( 0 [,) +oo ) ) ) )
46	45	ad2antrr	|- ( ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) /\ k e. y ) -> ( x e. A -> ( k e. B -> C e. ( 0 [,) +oo ) ) ) )
47	29 30 46	rexlimd	|- ( ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) /\ k e. y ) -> ( E. x e. A k e. B -> C e. ( 0 [,) +oo ) ) )
48	19 47	mpd	|- ( ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) /\ k e. y ) -> C e. ( 0 [,) +oo ) )
49	15 48	sge0fsummpt	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( k e. y |-> C ) ) = sum_ k e. y C )
50		sseqin2	|- ( y C_ U_ x e. A B <-> ( U_ x e. A B i^i y ) = y )
51	50	biimpi	|- ( y C_ U_ x e. A B -> ( U_ x e. A B i^i y ) = y )
52	51	eqcomd	|- ( y C_ U_ x e. A B -> y = ( U_ x e. A B i^i y ) )
53		iunin1	|- U_ x e. A ( B i^i y ) = ( U_ x e. A B i^i y )
54	53	a1i	|- ( y C_ U_ x e. A B -> U_ x e. A ( B i^i y ) = ( U_ x e. A B i^i y ) )
55	52 54	eqtr4d	|- ( y C_ U_ x e. A B -> y = U_ x e. A ( B i^i y ) )
56	10 55	syl	|- ( y e. ( ~P U_ x e. A B i^i Fin ) -> y = U_ x e. A ( B i^i y ) )
57	56	sumeq1d	|- ( y e. ( ~P U_ x e. A B i^i Fin ) -> sum_ k e. y C = sum_ k e. U_ x e. A ( B i^i y ) C )
58	57	adantl	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> sum_ k e. y C = sum_ k e. U_ x e. A ( B i^i y ) C )
59		simpl	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ph )
60	2	adantlr	|- ( ( ( ph /\ y e. Fin ) /\ x e. A ) -> B e. W )
61	3	adantr	|- ( ( ph /\ y e. Fin ) -> Disj_ x e. A B )
62		rge0ssre	|- ( 0 [,) +oo ) C_ RR
63		ax-resscn	|- RR C_ CC
64	62 63	sstri	|- ( 0 [,) +oo ) C_ CC
65	64 44	sselid	|- ( ( ph /\ x e. A /\ k e. B ) -> C e. CC )
66	65	3adant1r	|- ( ( ( ph /\ y e. Fin ) /\ x e. A /\ k e. B ) -> C e. CC )
67		simpr	|- ( ( ph /\ y e. Fin ) -> y e. Fin )
68	60 61 66 67	fsumiunss	|- ( ( ph /\ y e. Fin ) -> sum_ k e. U_ x e. A ( B i^i y ) C = sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C )
69	59 15 68	syl2anc	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> sum_ k e. U_ x e. A ( B i^i y ) C = sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C )
70	58 69	eqtrd	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> sum_ k e. y C = sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C )
71	13 49 70	3eqtrd	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( ( k e. U_ x e. A B |-> C ) |` y ) ) = sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C )
72	60 61 67	disjinfi	|- ( ( ph /\ y e. Fin ) -> { x e. A | ( B i^i y ) =/= (/) } e. Fin )
73		id	|- ( y e. Fin -> y e. Fin )
74		inss2	|- ( [_ w / x ]_ B i^i y ) C_ y
75	74	a1i	|- ( y e. Fin -> ( [_ w / x ]_ B i^i y ) C_ y )
76		ssfi	|- ( ( y e. Fin /\ ( [_ w / x ]_ B i^i y ) C_ y ) -> ( [_ w / x ]_ B i^i y ) e. Fin )
77	73 75 76	syl2anc	|- ( y e. Fin -> ( [_ w / x ]_ B i^i y ) e. Fin )
78	77	ad2antlr	|- ( ( ( ph /\ y e. Fin ) /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) -> ( [_ w / x ]_ B i^i y ) e. Fin )
79		simpll	|- ( ( ( ph /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> ph )
80		elrabi	|- ( w e. { x e. A | ( B i^i y ) =/= (/) } -> w e. A )
81	80	ad2antlr	|- ( ( ( ph /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> w e. A )
82		elinel1	|- ( k e. ( [_ w / x ]_ B i^i y ) -> k e. [_ w / x ]_ B )
83	82	adantl	|- ( ( ( ph /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> k e. [_ w / x ]_ B )
84		nfv	|- F/ x w e. A
85		nfcv	|- F/_ x k
86		nfcsb1v	|- F/_ x [_ w / x ]_ B
87	85 86	nfel	|- F/ x k e. [_ w / x ]_ B
88	20 84 87	nf3an	|- F/ x ( ph /\ w e. A /\ k e. [_ w / x ]_ B )
89	88 30	nfim	|- F/ x ( ( ph /\ w e. A /\ k e. [_ w / x ]_ B ) -> C e. ( 0 [,) +oo ) )
90		eleq1w	|- ( x = w -> ( x e. A <-> w e. A ) )
91		csbeq1a	|- ( x = w -> B = [_ w / x ]_ B )
92	91	eleq2d	|- ( x = w -> ( k e. B <-> k e. [_ w / x ]_ B ) )
93	90 92	3anbi23d	|- ( x = w -> ( ( ph /\ x e. A /\ k e. B ) <-> ( ph /\ w e. A /\ k e. [_ w / x ]_ B ) ) )
94	93	imbi1d	|- ( x = w -> ( ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,) +oo ) ) <-> ( ( ph /\ w e. A /\ k e. [_ w / x ]_ B ) -> C e. ( 0 [,) +oo ) ) ) )
95	89 94 44	chvarfv	|- ( ( ph /\ w e. A /\ k e. [_ w / x ]_ B ) -> C e. ( 0 [,) +oo ) )
96	79 81 83 95	syl3anc	|- ( ( ( ph /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> C e. ( 0 [,) +oo ) )
97	96	adantllr	|- ( ( ( ( ph /\ y e. Fin ) /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> C e. ( 0 [,) +oo ) )
98	78 97	fsumge0cl	|- ( ( ( ph /\ y e. Fin ) /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) -> sum_ k e. ( [_ w / x ]_ B i^i y ) C e. ( 0 [,) +oo ) )
99	72 98	sge0fsummpt	|- ( ( ph /\ y e. Fin ) -> ( sum^ ` ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( [_ w / x ]_ B i^i y ) C ) ) = sum_ w e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( [_ w / x ]_ B i^i y ) C )
100		inss2	|- ( B i^i y ) C_ y
101	100	a1i	|- ( y e. Fin -> ( B i^i y ) C_ y )
102		ssfi	|- ( ( y e. Fin /\ ( B i^i y ) C_ y ) -> ( B i^i y ) e. Fin )
103	73 101 102	syl2anc	|- ( y e. Fin -> ( B i^i y ) e. Fin )
104	103	ad2antlr	|- ( ( ( ph /\ y e. Fin ) /\ x e. { x e. A | ( B i^i y ) =/= (/) } ) -> ( B i^i y ) e. Fin )
105		simpll	|- ( ( ( ph /\ x e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( B i^i y ) ) -> ph )
106		rabid	|- ( x e. { x e. A | ( B i^i y ) =/= (/) } <-> ( x e. A /\ ( B i^i y ) =/= (/) ) )
107	106	biimpi	|- ( x e. { x e. A | ( B i^i y ) =/= (/) } -> ( x e. A /\ ( B i^i y ) =/= (/) ) )
108	107	simpld	|- ( x e. { x e. A | ( B i^i y ) =/= (/) } -> x e. A )
109	108	ad2antlr	|- ( ( ( ph /\ x e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( B i^i y ) ) -> x e. A )
110		elinel1	|- ( k e. ( B i^i y ) -> k e. B )
111	110	adantl	|- ( ( ( ph /\ x e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( B i^i y ) ) -> k e. B )
112	105 109 111 44	syl3anc	|- ( ( ( ph /\ x e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( B i^i y ) ) -> C e. ( 0 [,) +oo ) )
113	112	adantllr	|- ( ( ( ( ph /\ y e. Fin ) /\ x e. { x e. A | ( B i^i y ) =/= (/) } ) /\ k e. ( B i^i y ) ) -> C e. ( 0 [,) +oo ) )
114	104 113	sge0fsummpt	|- ( ( ( ph /\ y e. Fin ) /\ x e. { x e. A | ( B i^i y ) =/= (/) } ) -> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) = sum_ k e. ( B i^i y ) C )
115	114	mpteq2dva	|- ( ( ph /\ y e. Fin ) -> ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) = ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( B i^i y ) C ) )
116		nfrab1	|- F/_ x { x e. A | ( B i^i y ) =/= (/) }
117		nfcv	|- F/_ w { x e. A | ( B i^i y ) =/= (/) }
118		nfcv	|- F/_ w sum_ k e. ( B i^i y ) C
119	86 21	nfin	|- F/_ x ( [_ w / x ]_ B i^i y )
120		nfcv	|- F/_ x C
121	119 120	nfsum	|- F/_ x sum_ k e. ( [_ w / x ]_ B i^i y ) C
122	91	ineq1d	|- ( x = w -> ( B i^i y ) = ( [_ w / x ]_ B i^i y ) )
123	122	sumeq1d	|- ( x = w -> sum_ k e. ( B i^i y ) C = sum_ k e. ( [_ w / x ]_ B i^i y ) C )
124	116 117 118 121 123	cbvmptf	|- ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( B i^i y ) C ) = ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( [_ w / x ]_ B i^i y ) C )
125	124	a1i	|- ( ( ph /\ y e. Fin ) -> ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( B i^i y ) C ) = ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( [_ w / x ]_ B i^i y ) C ) )
126	115 125	eqtr2d	|- ( ( ph /\ y e. Fin ) -> ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( [_ w / x ]_ B i^i y ) C ) = ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) )
127	126	fveq2d	|- ( ( ph /\ y e. Fin ) -> ( sum^ ` ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( [_ w / x ]_ B i^i y ) C ) ) = ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) )
128	127	eqcomd	|- ( ( ph /\ y e. Fin ) -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) = ( sum^ ` ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> sum_ k e. ( [_ w / x ]_ B i^i y ) C ) ) )
129	123 117 116 118 121	cbvsum	|- sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C = sum_ w e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( [_ w / x ]_ B i^i y ) C
130	129	a1i	|- ( ( ph /\ y e. Fin ) -> sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C = sum_ w e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( [_ w / x ]_ B i^i y ) C )
131	99 128 130	3eqtr4d	|- ( ( ph /\ y e. Fin ) -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) = sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C )
132	59 15 131	syl2anc	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) = sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C )
133	132	eqcomd	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> sum_ x e. { x e. A | ( B i^i y ) =/= (/) } sum_ k e. ( B i^i y ) C = ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) )
134	71 133	eqtrd	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( ( k e. U_ x e. A B |-> C ) |` y ) ) = ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) )
135	80	ssriv	|- { x e. A | ( B i^i y ) =/= (/) } C_ A
136	135	a1i	|- ( ph -> { x e. A | ( B i^i y ) =/= (/) } C_ A )
137	1 136	ssexd	|- ( ph -> { x e. A | ( B i^i y ) =/= (/) } e. _V )
138		vex	|- y e. _V
139	138	inex2	|- ( [_ w / x ]_ B i^i y ) e. _V
140	139	a1i	|- ( ( ph /\ w e. A ) -> ( [_ w / x ]_ B i^i y ) e. _V )
141		icossicc	|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
142		simpll	|- ( ( ( ph /\ w e. A ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> ph )
143		simplr	|- ( ( ( ph /\ w e. A ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> w e. A )
144	82	adantl	|- ( ( ( ph /\ w e. A ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> k e. [_ w / x ]_ B )
145	142 143 144 95	syl3anc	|- ( ( ( ph /\ w e. A ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> C e. ( 0 [,) +oo ) )
146	141 145	sselid	|- ( ( ( ph /\ w e. A ) /\ k e. ( [_ w / x ]_ B i^i y ) ) -> C e. ( 0 [,] +oo ) )
147		eqid	|- ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) = ( k e. ( [_ w / x ]_ B i^i y ) |-> C )
148	146 147	fmptd	|- ( ( ph /\ w e. A ) -> ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) : ( [_ w / x ]_ B i^i y ) --> ( 0 [,] +oo ) )
149	140 148	sge0cl	|- ( ( ph /\ w e. A ) -> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) e. ( 0 [,] +oo ) )
150	80 149	sylan2	|- ( ( ph /\ w e. { x e. A | ( B i^i y ) =/= (/) } ) -> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) e. ( 0 [,] +oo ) )
151		nfcv	|- F/_ w ( sum^ ` ( k e. ( B i^i y ) |-> C ) )
152		nfcv	|- F/_ x sum^
153	119 120	nfmpt	|- F/_ x ( k e. ( [_ w / x ]_ B i^i y ) |-> C )
154	152 153	nffv	|- F/_ x ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) )
155	122	mpteq1d	|- ( x = w -> ( k e. ( B i^i y ) |-> C ) = ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) )
156	155	fveq2d	|- ( x = w -> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) = ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) )
157	116 117 151 154 156	cbvmptf	|- ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) = ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) )
158	150 157	fmptd	|- ( ph -> ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) : { x e. A | ( B i^i y ) =/= (/) } --> ( 0 [,] +oo ) )
159	137 158	sge0xrcl	|- ( ph -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) e. RR* )
160	159	adantr	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) e. RR* )
161		eqid	|- ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) = ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) )
162	149 161	fmptd	|- ( ph -> ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) : A --> ( 0 [,] +oo ) )
163	1 162	sge0xrcl	|- ( ph -> ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) e. RR* )
164	163	adantr	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) e. RR* )
165	59 7	syl	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) e. RR* )
166	157	fveq2i	|- ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) = ( sum^ ` ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) )
167	166	a1i	|- ( ph -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) = ( sum^ ` ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) )
168	1 149 136	sge0lessmpt	|- ( ph -> ( sum^ ` ( w e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) <_ ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) )
169	167 168	eqbrtrd	|- ( ph -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) <_ ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) )
170	169	adantr	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) <_ ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) )
171	151 154 156	cbvmpt	|- ( x e. A |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) = ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) )
172	171	eqcomi	|- ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) = ( x e. A |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) )
173	172	fveq2i	|- ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) )
174	173	a1i	|- ( ph -> ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) )
175	138	inex2	|- ( B i^i y ) e. _V
176	175	a1i	|- ( ( ph /\ x e. A ) -> ( B i^i y ) e. _V )
177	110 36	sylan2	|- ( ( ( ph /\ x e. A ) /\ k e. ( B i^i y ) ) -> C e. ( 0 [,] +oo ) )
178		eqid	|- ( k e. ( B i^i y ) |-> C ) = ( k e. ( B i^i y ) |-> C )
179	177 178	fmptd	|- ( ( ph /\ x e. A ) -> ( k e. ( B i^i y ) |-> C ) : ( B i^i y ) --> ( 0 [,] +oo ) )
180	176 179	sge0cl	|- ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) e. ( 0 [,] +oo ) )
181	2 37	sge0cl	|- ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,] +oo ) )
182		inss1	|- ( B i^i y ) C_ B
183	182	a1i	|- ( ( ph /\ x e. A ) -> ( B i^i y ) C_ B )
184	2 36 183	sge0lessmpt	|- ( ( ph /\ x e. A ) -> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) <_ ( sum^ ` ( k e. B |-> C ) ) )
185	20 1 180 181 184	sge0lempt	|- ( ph -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
186	174 185	eqbrtrd	|- ( ph -> ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
187	186	adantr	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( w e. A |-> ( sum^ ` ( k e. ( [_ w / x ]_ B i^i y ) |-> C ) ) ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
188	160 164 165 170 187	xrletrd	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( x e. { x e. A | ( B i^i y ) =/= (/) } |-> ( sum^ ` ( k e. ( B i^i y ) |-> C ) ) ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
189	134 188	eqbrtrd	|- ( ( ph /\ y e. ( ~P U_ x e. A B i^i Fin ) ) -> ( sum^ ` ( ( k e. U_ x e. A B |-> C ) |` y ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
190	189	ralrimiva	|- ( ph -> A. y e. ( ~P U_ x e. A B i^i Fin ) ( sum^ ` ( ( k e. U_ x e. A B |-> C ) |` y ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
191	9 8 7	sge0lefi	|- ( ph -> ( ( sum^ ` ( k e. U_ x e. A B |-> C ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) <-> A. y e. ( ~P U_ x e. A B i^i Fin ) ( sum^ ` ( ( k e. U_ x e. A B |-> C ) |` y ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) ) )
192	190 191	mpbird	|- ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) <_ ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
193		elpwinss	|- ( y e. ( ~P A i^i Fin ) -> y C_ A )
194	193	resmptd	|- ( y e. ( ~P A i^i Fin ) -> ( ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) |` y ) = ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) )
195	194	fveq2d	|- ( y e. ( ~P A i^i Fin ) -> ( sum^ ` ( ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) |` y ) ) = ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
196	195	adantl	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) |` y ) ) = ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
197		elinel2	|- ( y e. ( ~P A i^i Fin ) -> y e. Fin )
198	197	adantl	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
199		0xr	|- 0 e. RR*
200	199	a1i	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> 0 e. RR* )
201		pnfxr	|- +oo e. RR*
202	201	a1i	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> +oo e. RR* )
203		simpll	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ph )
204	193	sselda	|- ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> x e. A )
205	204	adantll	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> x e. A )
206	203 205 2	syl2anc	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> B e. W )
207	203 205 37	syl2anc	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ( k e. B |-> C ) : B --> ( 0 [,] +oo ) )
208	206 207	sge0xrcl	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR* )
209	206 207	sge0ge0	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> 0 <_ ( sum^ ` ( k e. B |-> C ) ) )
210	203 205 5	syl2anc	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ( sum^ ` ( k e. B |-> C ) ) e. RR )
211		ltpnf	|- ( ( sum^ ` ( k e. B |-> C ) ) e. RR -> ( sum^ ` ( k e. B |-> C ) ) < +oo )
212	210 211	syl	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ( sum^ ` ( k e. B |-> C ) ) < +oo )
213	200 202 208 209 212	elicod	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ( sum^ ` ( k e. B |-> C ) ) e. ( 0 [,) +oo ) )
214	198 213	sge0fsummpt	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) )
215	196 214	eqtrd	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) |` y ) ) = sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) )
216		nfv	|- F/ k ( ph /\ y e. ( ~P A i^i Fin ) )
217	9	adantr	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> U_ x e. A B e. _V )
218	8	fvmptelrn	|- ( ( ph /\ k e. U_ x e. A B ) -> C e. ( 0 [,] +oo ) )
219	218	adantlr	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. U_ x e. A B ) -> C e. ( 0 [,] +oo ) )
220	198 210	fsumrecl	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) e. RR )
221	220	rexrd	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) e. RR* )
222		nfv	|- F/ k ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ )
223		iunss1	|- ( y C_ A -> U_ x e. y B C_ U_ x e. A B )
224	193 223	syl	|- ( y e. ( ~P A i^i Fin ) -> U_ x e. y B C_ U_ x e. A B )
225	224	adantl	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> U_ x e. y B C_ U_ x e. A B )
226	217 225	ssexd	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> U_ x e. y B e. _V )
227	226	adantr	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> U_ x e. y B e. _V )
228		simpll	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. U_ x e. y B ) -> ph )
229	225	sselda	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. U_ x e. y B ) -> k e. U_ x e. A B )
230	228 229 218	syl2anc	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. U_ x e. y B ) -> C e. ( 0 [,] +oo ) )
231	230	adantlr	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ k e. U_ x e. y B ) -> C e. ( 0 [,] +oo ) )
232		simpr	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> p e. RR+ )
233	193	adantl	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
234	3	adantr	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> Disj_ x e. A B )
235		disjss1	|- ( y C_ A -> ( Disj_ x e. A B -> Disj_ x e. y B ) )
236	233 234 235	sylc	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> Disj_ x e. y B )
237	203	3adant3	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y /\ k e. B ) -> ph )
238	205	3adant3	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y /\ k e. B ) -> x e. A )
239		simp3	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y /\ k e. B ) -> k e. B )
240	237 238 239 4	syl3anc	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y /\ k e. B ) -> C e. ( 0 [,] +oo ) )
241	198 206 236 240 210	sge0iunmptlemfi	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) = ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )
242	214 220	eqeltrd	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( x e. y |-> ( sum^ ` ( k e. B |-> C ) ) ) ) e. RR )
243	241 242	eqeltrd	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) e. RR )
244	243	adantr	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) e. RR )
245	222 227 231 232 244	sge0ltfirpmpt	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> E. b e. ( ~P U_ x e. y B i^i Fin ) ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) )
246		nfv	|- F/ b ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ )
247		nfre1	|- F/ b E. b e. ( ~P U_ x e. A B i^i Fin ) sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p )
248	223	sspwd	|- ( y C_ A -> ~P U_ x e. y B C_ ~P U_ x e. A B )
249	193 248	syl	|- ( y e. ( ~P A i^i Fin ) -> ~P U_ x e. y B C_ ~P U_ x e. A B )
250	249	adantr	|- ( ( y e. ( ~P A i^i Fin ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ~P U_ x e. y B C_ ~P U_ x e. A B )
251		elinel1	|- ( b e. ( ~P U_ x e. y B i^i Fin ) -> b e. ~P U_ x e. y B )
252	251	adantl	|- ( ( y e. ( ~P A i^i Fin ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> b e. ~P U_ x e. y B )
253	250 252	sseldd	|- ( ( y e. ( ~P A i^i Fin ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> b e. ~P U_ x e. A B )
254		elinel2	|- ( b e. ( ~P U_ x e. y B i^i Fin ) -> b e. Fin )
255	254	adantl	|- ( ( y e. ( ~P A i^i Fin ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> b e. Fin )
256	253 255	elind	|- ( ( y e. ( ~P A i^i Fin ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> b e. ( ~P U_ x e. A B i^i Fin ) )
257	256	ad4ant24	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> b e. ( ~P U_ x e. A B i^i Fin ) )
258	257	3adant3	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> b e. ( ~P U_ x e. A B i^i Fin ) )
259	221	ad2antrr	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) e. RR* )
260	259	3adant3	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) e. RR* )
261		nfv	|- F/ k ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P U_ x e. y B i^i Fin ) )
262	226	adantr	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> U_ x e. y B e. _V )
263	230	adantlr	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) /\ k e. U_ x e. y B ) -> C e. ( 0 [,] +oo ) )
264	243	adantr	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) e. RR )
265	251	elpwid	|- ( b e. ( ~P U_ x e. y B i^i Fin ) -> b C_ U_ x e. y B )
266	265	adantl	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> b C_ U_ x e. y B )
267	261 262 263 264 266	sge0ssrempt	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ( sum^ ` ( k e. b |-> C ) ) e. RR )
268	267	rexrd	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ( sum^ ` ( k e. b |-> C ) ) e. RR* )
269	268	adantlr	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ( sum^ ` ( k e. b |-> C ) ) e. RR* )
270		rpxr	|- ( p e. RR+ -> p e. RR* )
271	270	ad2antlr	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> p e. RR* )
272	269 271	xaddcld	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ( ( sum^ ` ( k e. b |-> C ) ) +e p ) e. RR* )
273	272	3adant3	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> ( ( sum^ ` ( k e. b |-> C ) ) +e p ) e. RR* )
274		simp3	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) )
275	241 214	eqtr2d	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( k e. U_ x e. y B |-> C ) ) )
276	275	adantr	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( k e. U_ x e. y B |-> C ) ) )
277	276	3ad2ant1	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( k e. U_ x e. y B |-> C ) ) )
278	267	adantlr	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ( sum^ ` ( k e. b |-> C ) ) e. RR )
279		rpre	|- ( p e. RR+ -> p e. RR )
280	279	ad2antlr	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> p e. RR )
281		rexadd	|- ( ( ( sum^ ` ( k e. b |-> C ) ) e. RR /\ p e. RR ) -> ( ( sum^ ` ( k e. b |-> C ) ) +e p ) = ( ( sum^ ` ( k e. b |-> C ) ) + p ) )
282	278 280 281	syl2anc	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) ) -> ( ( sum^ ` ( k e. b |-> C ) ) +e p ) = ( ( sum^ ` ( k e. b |-> C ) ) + p ) )
283	282	3adant3	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> ( ( sum^ ` ( k e. b |-> C ) ) +e p ) = ( ( sum^ ` ( k e. b |-> C ) ) + p ) )
284	277 283	breq12d	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> ( sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) +e p ) <-> ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) )
285	274 284	mpbird	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) +e p ) )
286	260 273 285	xrltled	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p ) )
287		rspe	|- ( ( b e. ( ~P U_ x e. A B i^i Fin ) /\ sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p ) ) -> E. b e. ( ~P U_ x e. A B i^i Fin ) sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p ) )
288	258 286 287	syl2anc	|- ( ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) /\ b e. ( ~P U_ x e. y B i^i Fin ) /\ ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) ) -> E. b e. ( ~P U_ x e. A B i^i Fin ) sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p ) )
289	288	3exp	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> ( b e. ( ~P U_ x e. y B i^i Fin ) -> ( ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) -> E. b e. ( ~P U_ x e. A B i^i Fin ) sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p ) ) ) )
290	246 247 289	rexlimd	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> ( E. b e. ( ~P U_ x e. y B i^i Fin ) ( sum^ ` ( k e. U_ x e. y B |-> C ) ) < ( ( sum^ ` ( k e. b |-> C ) ) + p ) -> E. b e. ( ~P U_ x e. A B i^i Fin ) sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p ) ) )
291	245 290	mpd	|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ p e. RR+ ) -> E. b e. ( ~P U_ x e. A B i^i Fin ) sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( ( sum^ ` ( k e. b |-> C ) ) +e p ) )
292	216 217 219 221 291	sge0gerpmpt	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ x e. y ( sum^ ` ( k e. B |-> C ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
293	215 292	eqbrtrd	|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) |` y ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
294	293	ralrimiva	|- ( ph -> A. y e. ( ~P A i^i Fin ) ( sum^ ` ( ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) |` y ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
295		eqid	|- ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) )
296	181 295	fmptd	|- ( ph -> ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) : A --> ( 0 [,] +oo ) )
297	1 296 6	sge0lefi	|- ( ph -> ( ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) <-> A. y e. ( ~P A i^i Fin ) ( sum^ ` ( ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) |` y ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) ) )
298	294 297	mpbird	|- ( ph -> ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) <_ ( sum^ ` ( k e. U_ x e. A B |-> C ) ) )
299	6 7 192 298	xrletrid	|- ( ph -> ( sum^ ` ( k e. U_ x e. A B |-> C ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) )