Metamath Proof Explorer

Theorem omssubadd

Description: A constructed outer measure is countably sub-additive. Lemma 1.5.4 of Bogachev p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019) (Revised by AV, 4-Oct-2020) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

Ref Expression
Hypotheses oms.m 
|- M = ( toOMeas ` R )
oms.o 
|- ( ph -> Q e. V )
oms.r 
|- ( ph -> R : Q --> ( 0 [,] +oo ) )
omssubadd.a 
|- ( ( ph /\ y e. X ) -> A C_ U. Q )
omssubadd.b 
|- ( ph -> X ~<_ _om )
Assertion omssubadd 
|- ( ph -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )

Proof

Step Hyp Ref Expression
1 oms.m 
 |-  M = ( toOMeas ` R )
2 oms.o 
 |-  ( ph -> Q e. V )
3 oms.r 
 |-  ( ph -> R : Q --> ( 0 [,] +oo ) )
4 omssubadd.a 
 |-  ( ( ph /\ y e. X ) -> A C_ U. Q )
5 omssubadd.b 
 |-  ( ph -> X ~<_ _om )
6 nnenom 
 |-  NN ~~ _om
7 domen2 
 |-  ( NN ~~ _om -> ( X ~<_ NN <-> X ~<_ _om ) )
8 6 7 ax-mp 
 |-  ( X ~<_ NN <-> X ~<_ _om )
9 5 8 sylibr 
 |-  ( ph -> X ~<_ NN )
10 brdomi 
 |-  ( X ~<_ NN -> E. f f : X -1-1-> NN )
11 9 10 syl 
 |-  ( ph -> E. f f : X -1-1-> NN )
12 11 adantr 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> E. f f : X -1-1-> NN )
13 simplll 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ph )
14 ctex 
 |-  ( X ~<_ _om -> X e. _V )
15 5 14 syl 
 |-  ( ph -> X e. _V )
16 13 15 syl 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> X e. _V )
17 3 2 fexd 
 |-  ( ph -> R e. _V )
18 dmexg 
 |-  ( R e. _V -> dom R e. _V )
19 pwexg 
 |-  ( dom R e. _V -> ~P dom R e. _V )
20 17 18 19 3syl 
 |-  ( ph -> ~P dom R e. _V )
21 rabexg 
 |-  ( ~P dom R e. _V -> { z e. ~P dom R | z ~<_ _om } e. _V )
22 20 21 syl 
 |-  ( ph -> { z e. ~P dom R | z ~<_ _om } e. _V )
23 22 ad3antrrr 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> { z e. ~P dom R | z ~<_ _om } e. _V )
24 nfv 
 |-  F/ y ph
25 nfcv 
 |-  F/_ y X
26 25 nfesum1 
 |-  F/_ y sum* y e. X ( M ` A )
27 26 nfel1 
 |-  F/ y sum* y e. X ( M ` A ) e. RR
28 24 27 nfan 
 |-  F/ y ( ph /\ sum* y e. X ( M ` A ) e. RR )
29 nfv 
 |-  F/ y f : X -1-1-> NN
30 28 29 nfan 
 |-  F/ y ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN )
31 nfv 
 |-  F/ y e e. RR+
32 30 31 nfan 
 |-  F/ y ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ )
33 13 adantr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ph )
34 simpr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> y e. X )
35 15 adantr 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> X e. _V )
36 omsf 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
37 1 feq1i 
 |-  ( M : ~P U. dom R --> ( 0 [,] +oo ) <-> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
38 36 37 sylibr 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
39 2 3 38 syl2anc 
 |-  ( ph -> M : ~P U. dom R --> ( 0 [,] +oo ) )
40 39 adantr 
 |-  ( ( ph /\ y e. X ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
41 2 uniexd 
 |-  ( ph -> U. Q e. _V )
42 41 adantr 
 |-  ( ( ph /\ y e. X ) -> U. Q e. _V )
43 42 4 ssexd 
 |-  ( ( ph /\ y e. X ) -> A e. _V )
44 3 fdmd 
 |-  ( ph -> dom R = Q )
45 44 unieqd 
 |-  ( ph -> U. dom R = U. Q )
46 45 adantr 
 |-  ( ( ph /\ y e. X ) -> U. dom R = U. Q )
47 4 46 sseqtrrd 
 |-  ( ( ph /\ y e. X ) -> A C_ U. dom R )
48 43 47 elpwd 
 |-  ( ( ph /\ y e. X ) -> A e. ~P U. dom R )
49 40 48 ffvelcdmd 
 |-  ( ( ph /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
50 49 adantlr 
 |-  ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
51 simpr 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> sum* y e. X ( M ` A ) e. RR )
52 28 35 50 51 esumcvgre 
 |-  ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. RR )
53 52 ad4ant14 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) e. RR )
54 simplr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
55 2rp 
 |-  2 e. RR+
56 55 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. RR+ )
57 f1f 
 |-  ( f : X -1-1-> NN -> f : X --> NN )
58 57 adantl 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> f : X --> NN )
59 58 ffvelcdmda 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. NN )
60 59 nnzd 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
61 56 60 rpexpcld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
62 61 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
63 54 62 rpdivcld 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR+ )
64 63 rpred 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
65 64 adantl3r 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
66 53 65 rexaddd 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) = ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
67 49 ad5ant15 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
68 dfrp2 
 |-  RR+ = ( 0 (,) +oo )
69 ioossicc 
 |-  ( 0 (,) +oo ) C_ ( 0 [,] +oo )
70 68 69 eqsstri 
 |-  RR+ C_ ( 0 [,] +oo )
71 70 63 sselid 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
72 71 adantl3r 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
73 67 72 xrge0addcld 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
74 66 73 eqeltrrd 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
75 1 fveq1i 
 |-  ( M ` A ) = ( ( toOMeas ` R ) ` A )
76 2 adantr 
 |-  ( ( ph /\ y e. X ) -> Q e. V )
77 3 adantr 
 |-  ( ( ph /\ y e. X ) -> R : Q --> ( 0 [,] +oo ) )
78 omsfval 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( ( toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
79 76 77 4 78 syl3anc 
 |-  ( ( ph /\ y e. X ) -> ( ( toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
80 75 79 eqtrid 
 |-  ( ( ph /\ y e. X ) -> ( M ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
81 80 ad5ant15 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
82 54 rpred 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
83 82 adantl3r 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
84 61 rpred 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
85 84 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
86 85 adantl3r 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
87 simplr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
88 87 rpgt0d 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < e )
89 2re 
 |-  2 e. RR
90 60 adantllr 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
91 90 adantlr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( f ` y ) e. ZZ )
92 2pos 
 |-  0 < 2
93 92 a1i 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < 2 )
94 expgt0 
 |-  ( ( 2 e. RR /\ ( f ` y ) e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ ( f ` y ) ) )
95 89 91 93 94 mp3an2i 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < ( 2 ^ ( f ` y ) ) )
96 83 86 88 95 divgt0d 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < ( e / ( 2 ^ ( f ` y ) ) ) )
97 65 53 ltaddposd 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 0 < ( e / ( 2 ^ ( f ` y ) ) ) <-> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
98 96 97 mpbid 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
99 81 98 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
100 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
101 xrltso 
 |-  < Or RR*
102 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
103 100 101 102 mp2 
 |-  < Or ( 0 [,] +oo )
104 103 a1i 
 |-  ( ( ph /\ y e. X ) -> < Or ( 0 [,] +oo ) )
105 omscl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
106 76 77 48 105 syl3anc 
 |-  ( ( ph /\ y e. X ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
107 xrge0infss 
 |-  ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) -> E. v e. ( 0 [,] +oo ) ( A. h e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -. h < v /\ A. h e. ( 0 [,] +oo ) ( v < h -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < h ) ) )
108 106 107 syl 
 |-  ( ( ph /\ y e. X ) -> E. v e. ( 0 [,] +oo ) ( A. h e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -. h < v /\ A. h e. ( 0 [,] +oo ) ( v < h -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < h ) ) )
109 104 108 infglb 
 |-  ( ( ph /\ y e. X ) -> ( ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) /\ inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
110 109 imp 
 |-  ( ( ( ph /\ y e. X ) /\ ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) /\ inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
111 33 34 74 99 110 syl22anc 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
112 eqid 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) = ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) )
113 esumex 
 |-  sum* w e. x ( R ` w ) e. _V
114 112 113 elrnmpti 
 |-  ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } u = sum* w e. x ( R ` w ) )
115 114 anbi1i 
 |-  ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
116 r19.41v 
 |-  ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
117 115 116 bitr4i 
 |-  ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
118 117 exbii 
 |-  ( E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
119 df-rex 
 |-  ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
120 rexcom4 
 |-  ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
121 118 119 120 3bitr4i 
 |-  ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
122 breq1 
 |-  ( u = sum* w e. x ( R ` w ) -> ( u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
123 122 biimpa 
 |-  ( ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
124 123 exlimiv 
 |-  ( E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
125 124 reximi 
 |-  ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
126 121 125 sylbi 
 |-  ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
127 111 126 syl 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
128 simpr 
 |-  ( ( A C_ U. z /\ z ~<_ _om ) -> z ~<_ _om )
129 128 a1i 
 |-  ( z e. ~P dom R -> ( ( A C_ U. z /\ z ~<_ _om ) -> z ~<_ _om ) )
130 129 ss2rabi 
 |-  { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } C_ { z e. ~P dom R | z ~<_ _om }
131 rexss 
 |-  ( { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } C_ { z e. ~P dom R | z ~<_ _om } -> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. x e. { z e. ~P dom R | z ~<_ _om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
132 130 131 ax-mp 
 |-  ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. x e. { z e. ~P dom R | z ~<_ _om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
133 unieq 
 |-  ( z = x -> U. z = U. x )
134 133 sseq2d 
 |-  ( z = x -> ( A C_ U. z <-> A C_ U. x ) )
135 breq1 
 |-  ( z = x -> ( z ~<_ _om <-> x ~<_ _om ) )
136 134 135 anbi12d 
 |-  ( z = x -> ( ( A C_ U. z /\ z ~<_ _om ) <-> ( A C_ U. x /\ x ~<_ _om ) ) )
137 136 elrab 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } <-> ( x e. ~P dom R /\ ( A C_ U. x /\ x ~<_ _om ) ) )
138 137 simprbi 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } -> ( A C_ U. x /\ x ~<_ _om ) )
139 138 simpld 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } -> A C_ U. x )
140 139 a1i 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } -> A C_ U. x ) )
141 140 anim1d 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( A C_ U. x /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
142 141 reximdv 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( E. x e. { z e. ~P dom R | z ~<_ _om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> E. x e. { z e. ~P dom R | z ~<_ _om } ( A C_ U. x /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
143 132 142 biimtrid 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> E. x e. { z e. ~P dom R | z ~<_ _om } ( A C_ U. x /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
144 127 143 mpd 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> E. x e. { z e. ~P dom R | z ~<_ _om } ( A C_ U. x /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
145 32 144 ralrimia 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> A. y e. X E. x e. { z e. ~P dom R | z ~<_ _om } ( A C_ U. x /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
146 unieq 
 |-  ( x = ( g ` y ) -> U. x = U. ( g ` y ) )
147 146 sseq2d 
 |-  ( x = ( g ` y ) -> ( A C_ U. x <-> A C_ U. ( g ` y ) ) )
148 esumeq1 
 |-  ( x = ( g ` y ) -> sum* w e. x ( R ` w ) = sum* w e. ( g ` y ) ( R ` w ) )
149 148 breq1d 
 |-  ( x = ( g ` y ) -> ( sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
150 147 149 anbi12d 
 |-  ( x = ( g ` y ) -> ( ( A C_ U. x /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
151 150 ac6 
 |-  ( ( X e. _V /\ { z e. ~P dom R | z ~<_ _om } e. _V /\ A. y e. X E. x e. { z e. ~P dom R | z ~<_ _om } ( A C_ U. x /\ sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> E. g ( g : X --> { z e. ~P dom R | z ~<_ _om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
152 16 23 145 151 syl3anc 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> E. g ( g : X --> { z e. ~P dom R | z ~<_ _om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
153 simp-5l 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ph )
154 43 ralrimiva 
 |-  ( ph -> A. y e. X A e. _V )
155 iunexg 
 |-  ( ( X e. _V /\ A. y e. X A e. _V ) -> U_ y e. X A e. _V )
156 15 154 155 syl2anc 
 |-  ( ph -> U_ y e. X A e. _V )
157 47 iunssd 
 |-  ( ph -> U_ y e. X A C_ U. dom R )
158 156 157 elpwd 
 |-  ( ph -> U_ y e. X A e. ~P U. dom R )
159 39 158 ffvelcdmd 
 |-  ( ph -> ( M ` U_ y e. X A ) e. ( 0 [,] +oo ) )
160 100 159 sselid 
 |-  ( ph -> ( M ` U_ y e. X A ) e. RR* )
161 153 160 syl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) e. RR* )
162 simplr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> g : X --> { z e. ~P dom R | z ~<_ _om } )
163 35 ad4antr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> X e. _V )
164 162 163 fexd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> g e. _V )
165 rnexg 
 |-  ( g e. _V -> ran g e. _V )
166 uniexg 
 |-  ( ran g e. _V -> U. ran g e. _V )
167 164 165 166 3syl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g e. _V )
168 3 ad2antrr 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ c e. U. ran g ) -> R : Q --> ( 0 [,] +oo ) )
169 frn 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> ran g C_ { z e. ~P dom R | z ~<_ _om } )
170 ssrab2 
 |-  { z e. ~P dom R | z ~<_ _om } C_ ~P dom R
171 169 170 sstrdi 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> ran g C_ ~P dom R )
172 171 unissd 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> U. ran g C_ U. ~P dom R )
173 unipw 
 |-  U. ~P dom R = dom R
174 172 173 sseqtrdi 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> U. ran g C_ dom R )
175 174 adantl 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> U. ran g C_ dom R )
176 44 adantr 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> dom R = Q )
177 175 176 sseqtrd 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> U. ran g C_ Q )
178 177 sselda 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ c e. U. ran g ) -> c e. Q )
179 168 178 ffvelcdmd 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ c e. U. ran g ) -> ( R ` c ) e. ( 0 [,] +oo ) )
180 179 ralrimiva 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
181 153 162 180 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
182 nfcv 
 |-  F/_ c U. ran g
183 182 esumcl 
 |-  ( ( U. ran g e. _V /\ A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) ) -> sum* c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
184 167 181 183 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
185 100 184 sselid 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* c e. U. ran g ( R ` c ) e. RR* )
186 simp-5r 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( M ` A ) e. RR )
187 186 rexrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( M ` A ) e. RR* )
188 simpllr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> e e. RR+ )
189 188 rpxrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> e e. RR* )
190 187 189 xaddcld 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( sum* y e. X ( M ` A ) +e e ) e. RR* )
191 169 ad2antlr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ran g C_ { z e. ~P dom R | z ~<_ _om } )
192 sstr 
 |-  ( ( ran g C_ { z e. ~P dom R | z ~<_ _om } /\ { z e. ~P dom R | z ~<_ _om } C_ ~P dom R ) -> ran g C_ ~P dom R )
193 170 192 mpan2 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } -> ran g C_ ~P dom R )
194 sspwuni 
 |-  ( ran g C_ ~P dom R <-> U. ran g C_ dom R )
195 193 194 sylib 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } -> U. ran g C_ dom R )
196 191 195 syl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g C_ dom R )
197 ffn 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> g Fn X )
198 197 ad2antlr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> g Fn X )
199 153 5 syl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> X ~<_ _om )
200 fnct 
 |-  ( ( g Fn X /\ X ~<_ _om ) -> g ~<_ _om )
201 rnct 
 |-  ( g ~<_ _om -> ran g ~<_ _om )
202 200 201 syl 
 |-  ( ( g Fn X /\ X ~<_ _om ) -> ran g ~<_ _om )
203 dfss3 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } <-> A. w e. ran g w e. { z e. ~P dom R | z ~<_ _om } )
204 breq1 
 |-  ( z = w -> ( z ~<_ _om <-> w ~<_ _om ) )
205 204 elrab 
 |-  ( w e. { z e. ~P dom R | z ~<_ _om } <-> ( w e. ~P dom R /\ w ~<_ _om ) )
206 205 simprbi 
 |-  ( w e. { z e. ~P dom R | z ~<_ _om } -> w ~<_ _om )
207 206 ralimi 
 |-  ( A. w e. ran g w e. { z e. ~P dom R | z ~<_ _om } -> A. w e. ran g w ~<_ _om )
208 203 207 sylbi 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } -> A. w e. ran g w ~<_ _om )
209 unictb 
 |-  ( ( ran g ~<_ _om /\ A. w e. ran g w ~<_ _om ) -> U. ran g ~<_ _om )
210 202 208 209 syl2an 
 |-  ( ( ( g Fn X /\ X ~<_ _om ) /\ ran g C_ { z e. ~P dom R | z ~<_ _om } ) -> U. ran g ~<_ _om )
211 198 199 191 210 syl21anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g ~<_ _om )
212 ctex 
 |-  ( U. ran g ~<_ _om -> U. ran g e. _V )
213 elpwg 
 |-  ( U. ran g e. _V -> ( U. ran g e. ~P dom R <-> U. ran g C_ dom R ) )
214 211 212 213 3syl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( U. ran g e. ~P dom R <-> U. ran g C_ dom R ) )
215 196 214 mpbird 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g e. ~P dom R )
216 simpl 
 |-  ( ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A C_ U. ( g ` y ) )
217 216 ralimi 
 |-  ( A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A. y e. X A C_ U. ( g ` y ) )
218 fvssunirn 
 |-  ( g ` y ) C_ U. ran g
219 218 unissi 
 |-  U. ( g ` y ) C_ U. U. ran g
220 sstr 
 |-  ( ( A C_ U. ( g ` y ) /\ U. ( g ` y ) C_ U. U. ran g ) -> A C_ U. U. ran g )
221 219 220 mpan2 
 |-  ( A C_ U. ( g ` y ) -> A C_ U. U. ran g )
222 221 ralimi 
 |-  ( A. y e. X A C_ U. ( g ` y ) -> A. y e. X A C_ U. U. ran g )
223 iunss 
 |-  ( U_ y e. X A C_ U. U. ran g <-> A. y e. X A C_ U. U. ran g )
224 222 223 sylibr 
 |-  ( A. y e. X A C_ U. ( g ` y ) -> U_ y e. X A C_ U. U. ran g )
225 217 224 syl 
 |-  ( A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> U_ y e. X A C_ U. U. ran g )
226 225 adantl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U_ y e. X A C_ U. U. ran g )
227 215 226 211 jca32 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( U. ran g e. ~P dom R /\ ( U_ y e. X A C_ U. U. ran g /\ U. ran g ~<_ _om ) ) )
228 unieq 
 |-  ( z = U. ran g -> U. z = U. U. ran g )
229 228 sseq2d 
 |-  ( z = U. ran g -> ( U_ y e. X A C_ U. z <-> U_ y e. X A C_ U. U. ran g ) )
230 breq1 
 |-  ( z = U. ran g -> ( z ~<_ _om <-> U. ran g ~<_ _om ) )
231 229 230 anbi12d 
 |-  ( z = U. ran g -> ( ( U_ y e. X A C_ U. z /\ z ~<_ _om ) <-> ( U_ y e. X A C_ U. U. ran g /\ U. ran g ~<_ _om ) ) )
232 231 elrab 
 |-  ( U. ran g e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } <-> ( U. ran g e. ~P dom R /\ ( U_ y e. X A C_ U. U. ran g /\ U. ran g ~<_ _om ) ) )
233 227 232 sylibr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } )
234 fveq2 
 |-  ( c = w -> ( R ` c ) = ( R ` w ) )
235 234 cbvesumv 
 |-  sum* c e. U. ran g ( R ` c ) = sum* w e. U. ran g ( R ` w )
236 esumeq1 
 |-  ( x = U. ran g -> sum* w e. x ( R ` w ) = sum* w e. U. ran g ( R ` w ) )
237 236 rspceeqv 
 |-  ( ( U. ran g e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } /\ sum* c e. U. ran g ( R ` c ) = sum* w e. U. ran g ( R ` w ) ) -> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } sum* c e. U. ran g ( R ` c ) = sum* w e. x ( R ` w ) )
238 233 235 237 sylancl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } sum* c e. U. ran g ( R ` c ) = sum* w e. x ( R ` w ) )
239 esumex 
 |-  sum* c e. U. ran g ( R ` c ) e. _V
240 eqid 
 |-  ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) = ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) )
241 240 elrnmpt 
 |-  ( sum* c e. U. ran g ( R ` c ) e. _V -> ( sum* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) <-> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } sum* c e. U. ran g ( R ` c ) = sum* w e. x ( R ` w ) ) )
242 239 241 ax-mp 
 |-  ( sum* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) <-> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } sum* c e. U. ran g ( R ` c ) = sum* w e. x ( R ` w ) )
243 238 242 sylibr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) )
244 103 a1i 
 |-  ( ph -> < Or ( 0 [,] +oo ) )
245 omscl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ U_ y e. X A e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
246 2 3 158 245 syl3anc 
 |-  ( ph -> ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
247 xrge0infss 
 |-  ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -. t < e /\ A. t e. ( 0 [,] +oo ) ( e < t -> E. u e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < t ) ) )
248 246 247 syl 
 |-  ( ph -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -. t < e /\ A. t e. ( 0 [,] +oo ) ( e < t -> E. u e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < t ) ) )
249 244 248 inflb 
 |-  ( ph -> ( sum* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -> -. sum* c e. U. ran g ( R ` c ) < inf ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) ) )
250 1 fveq1i 
 |-  ( M ` U_ y e. X A ) = ( ( toOMeas ` R ) ` U_ y e. X A )
251 4 iunssd 
 |-  ( ph -> U_ y e. X A C_ U. Q )
252 omsfval 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ U_ y e. X A C_ U. Q ) -> ( ( toOMeas ` R ) ` U_ y e. X A ) = inf ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
253 2 3 251 252 syl3anc 
 |-  ( ph -> ( ( toOMeas ` R ) ` U_ y e. X A ) = inf ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
254 250 253 eqtrid 
 |-  ( ph -> ( M ` U_ y e. X A ) = inf ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
255 254 breq2d 
 |-  ( ph -> ( sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) <-> sum* c e. U. ran g ( R ` c ) < inf ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) ) )
256 255 notbid 
 |-  ( ph -> ( -. sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) <-> -. sum* c e. U. ran g ( R ` c ) < inf ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) ) )
257 249 256 sylibrd 
 |-  ( ph -> ( sum* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -> -. sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) ) )
258 153 243 257 sylc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> -. sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
259 161 185 258 xrnltled 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ sum* c e. U. ran g ( R ` c ) )
260 nfv 
 |-  F/ y g : X --> { z e. ~P dom R | z ~<_ _om }
261 32 260 nfan 
 |-  F/ y ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } )
262 nfra1 
 |-  F/ y A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
263 261 262 nfan 
 |-  F/ y ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
264 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ph )
265 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> g : X --> { z e. ~P dom R | z ~<_ _om } )
266 simpr 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> y e. X )
267 fvex 
 |-  ( g ` y ) e. _V
268 3 ad3antrrr 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> R : Q --> ( 0 [,] +oo ) )
269 simpllr 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> g : X --> { z e. ~P dom R | z ~<_ _om } )
270 simplr 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> y e. X )
271 269 270 ffvelcdmd 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) e. { z e. ~P dom R | z ~<_ _om } )
272 170 271 sselid 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) e. ~P dom R )
273 272 elpwid 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ dom R )
274 268 273 fssdmd 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ Q )
275 simpr 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. ( g ` y ) )
276 274 275 sseldd 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. Q )
277 268 276 ffvelcdmd 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( R ` w ) e. ( 0 [,] +oo ) )
278 277 ralrimiva 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> A. w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
279 nfcv 
 |-  F/_ w ( g ` y )
280 279 esumcl 
 |-  ( ( ( g ` y ) e. _V /\ A. w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) ) -> sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
281 267 278 280 sylancr 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
282 264 265 266 281 syl21anc 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
283 263 282 ralrimia 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
284 25 esumcl 
 |-  ( ( X e. _V /\ A. y e. X sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) ) -> sum* y e. X sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
285 163 283 284 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
286 100 285 sselid 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X sum* w e. ( g ` y ) ( R ` w ) e. RR* )
287 nfv 
 |-  F/ w ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } )
288 simpr 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> g : X --> { z e. ~P dom R | z ~<_ _om } )
289 fniunfv 
 |-  ( g Fn X -> U_ y e. X ( g ` y ) = U. ran g )
290 288 197 289 3syl 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> U_ y e. X ( g ` y ) = U. ran g )
291 287 290 esumeq1d 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> sum* w e. U_ y e. X ( g ` y ) ( R ` w ) = sum* w e. U. ran g ( R ` w ) )
292 15 adantr 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> X e. _V )
293 267 a1i 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( g ` y ) e. _V )
294 292 293 277 esumiun 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> sum* w e. U_ y e. X ( g ` y ) ( R ` w ) <_ sum* y e. X sum* w e. ( g ` y ) ( R ` w ) )
295 291 294 eqbrtrrd 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> sum* w e. U. ran g ( R ` w ) <_ sum* y e. X sum* w e. ( g ` y ) ( R ` w ) )
296 295 ad5ant15 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> sum* w e. U. ran g ( R ` w ) <_ sum* y e. X sum* w e. ( g ` y ) ( R ` w ) )
297 296 adantr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* w e. U. ran g ( R ` w ) <_ sum* y e. X sum* w e. ( g ` y ) ( R ` w ) )
298 235 297 eqbrtrid 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* c e. U. ran g ( R ` c ) <_ sum* y e. X sum* w e. ( g ` y ) ( R ` w ) )
299 264 266 49 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
300 72 ad4ant14 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
301 299 300 xrge0addcld 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
302 263 301 ralrimia 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
303 25 esumcl 
 |-  ( ( X e. _V /\ A. y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) ) -> sum* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
304 163 302 303 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
305 100 304 sselid 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. RR* )
306 199 14 syl 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> X e. _V )
307 52 ad5ant15 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( M ` A ) e. RR )
308 307 adantr 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( M ` A ) e. RR )
309 65 adantlr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
310 309 adantr 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
311 simpr 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
312 rexadd 
 |-  ( ( ( M ` A ) e. RR /\ ( e / ( 2 ^ ( f ` y ) ) ) e. RR ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) = ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
313 312 breq2d 
 |-  ( ( ( M ` A ) e. RR /\ ( e / ( 2 ^ ( f ` y ) ) ) e. RR ) -> ( sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) <-> sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
314 313 biimpar 
 |-  ( ( ( ( M ` A ) e. RR /\ ( e / ( 2 ^ ( f ` y ) ) ) e. RR ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
315 308 310 311 314 syl21anc 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
316 315 ex 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
317 simp-5l 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ph )
318 simplr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> g : X --> { z e. ~P dom R | z ~<_ _om } )
319 simpr 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> y e. X )
320 317 318 319 281 syl21anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
321 100 320 sselid 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> sum* w e. ( g ` y ) ( R ` w ) e. RR* )
322 307 rexrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( M ` A ) e. RR* )
323 309 rexrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR* )
324 322 323 xaddcld 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. RR* )
325 xrltle 
 |-  ( ( sum* w e. ( g ` y ) ( R ` w ) e. RR* /\ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. RR* ) -> ( sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
326 321 324 325 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
327 316 326 syld 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
328 327 adantld 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
329 261 328 ralimdaa 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> ( A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A. y e. X sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
330 329 imp 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
331 330 r19.21bi 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
332 263 25 306 282 301 331 esumlef 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X sum* w e. ( g ` y ) ( R ` w ) <_ sum* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
333 153 49 sylan 
 |-  ( ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
334 263 25 306 333 300 esumaddf 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) = ( sum* y e. X ( M ` A ) +e sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) ) )
335 263 300 ralrimia 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
336 25 esumcl 
 |-  ( ( X e. _V /\ A. y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) ) -> sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
337 163 335 336 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
338 100 337 sselid 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. RR* )
339 simp-4r 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> f : X -1-1-> NN )
340 vex 
 |-  f e. _V
341 340 rnex 
 |-  ran f e. _V
342 58 frnd 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> ran f C_ NN )
343 342 adantr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ran f C_ NN )
344 343 sselda 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. ran f ) -> z e. NN )
345 55 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> 2 e. RR+ )
346 simpr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> z e. NN )
347 346 nnzd 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> z e. ZZ )
348 345 347 rpexpcld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 2 ^ z ) e. RR+ )
349 348 rpreccld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. RR+ )
350 70 349 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
351 350 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
352 344 351 syldan 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. ran f ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
353 352 ralrimiva 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> A. z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
354 nfcv 
 |-  F/_ z ran f
355 354 esumcl 
 |-  ( ( ran f e. _V /\ A. z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
356 341 353 355 sylancr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
357 100 356 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) e. RR* )
358 1xr 
 |-  1 e. RR*
359 358 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> 1 e. RR* )
360 70 sseli 
 |-  ( e e. RR+ -> e e. ( 0 [,] +oo ) )
361 360 adantl 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. ( 0 [,] +oo ) )
362 elxrge0 
 |-  ( e e. ( 0 [,] +oo ) <-> ( e e. RR* /\ 0 <_ e ) )
363 361 362 sylib 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e e. RR* /\ 0 <_ e ) )
364 nfv 
 |-  F/ z ( ph /\ f : X -1-1-> NN )
365 nnex 
 |-  NN e. _V
366 365 a1i 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> NN e. _V )
367 364 366 350 342 esummono 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) <_ sum* z e. NN ( 1 / ( 2 ^ z ) ) )
368 oveq2 
 |-  ( z = w -> ( 2 ^ z ) = ( 2 ^ w ) )
369 368 oveq2d 
 |-  ( z = w -> ( 1 / ( 2 ^ z ) ) = ( 1 / ( 2 ^ w ) ) )
370 ioossico 
 |-  ( 0 (,) +oo ) C_ ( 0 [,) +oo )
371 68 370 eqsstri 
 |-  RR+ C_ ( 0 [,) +oo )
372 371 349 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,) +oo ) )
373 eqidd 
 |-  ( z e. NN -> ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) = ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) )
374 simpr 
 |-  ( ( z e. NN /\ w = z ) -> w = z )
375 374 oveq2d 
 |-  ( ( z e. NN /\ w = z ) -> ( 2 ^ w ) = ( 2 ^ z ) )
376 375 oveq2d 
 |-  ( ( z e. NN /\ w = z ) -> ( 1 / ( 2 ^ w ) ) = ( 1 / ( 2 ^ z ) ) )
377 id 
 |-  ( z e. NN -> z e. NN )
378 ovexd 
 |-  ( z e. NN -> ( 1 / ( 2 ^ z ) ) e. _V )
379 373 376 377 378 fvmptd 
 |-  ( z e. NN -> ( ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ` z ) = ( 1 / ( 2 ^ z ) ) )
380 379 adantl 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ` z ) = ( 1 / ( 2 ^ z ) ) )
381 ax-1cn 
 |-  1 e. CC
382 eqid 
 |-  ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) = ( w e. NN |-> ( 1 / ( 2 ^ w ) ) )
383 382 geo2lim 
 |-  ( 1 e. CC -> seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1 )
384 381 383 mp1i 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1 )
385 1red 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> 1 e. RR )
386 369 372 380 384 385 esumcvgsum 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. NN ( 1 / ( 2 ^ z ) ) = sum_ z e. NN ( 1 / ( 2 ^ z ) ) )
387 geoihalfsum 
 |-  sum_ z e. NN ( 1 / ( 2 ^ z ) ) = 1
388 386 387 eqtrdi 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. NN ( 1 / ( 2 ^ z ) ) = 1 )
389 367 388 breqtrd 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 )
390 389 adantr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 )
391 xlemul2a 
 |-  ( ( ( sum* z e. ran f ( 1 / ( 2 ^ z ) ) e. RR* /\ 1 e. RR* /\ ( e e. RR* /\ 0 <_ e ) ) /\ sum* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 ) -> ( e *e sum* z e. ran f ( 1 / ( 2 ^ z ) ) ) <_ ( e *e 1 ) )
392 357 359 363 390 391 syl31anc 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e *e sum* z e. ran f ( 1 / ( 2 ^ z ) ) ) <_ ( e *e 1 ) )
393 54 rpcnd 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. CC )
394 61 rpcnd 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. CC )
395 394 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. CC )
396 2cnd 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. CC )
397 2ne0 
 |-  2 =/= 0
398 397 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 =/= 0 )
399 396 398 60 expne0d 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) =/= 0 )
400 399 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) =/= 0 )
401 393 395 400 divrecd 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
402 61 rpreccld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR+ )
403 402 rpred 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR )
404 403 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR )
405 rexmul 
 |-  ( ( e e. RR /\ ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR ) -> ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
406 82 404 405 syl2anc 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
407 401 406 eqtr4d 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) = ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
408 407 esumeq2dv 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) = sum* y e. X ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
409 15 ad2antrr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> X e. _V )
410 70 402 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
411 410 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
412 371 a1i 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> RR+ C_ ( 0 [,) +oo ) )
413 412 sselda 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. ( 0 [,) +oo ) )
414 409 411 413 esummulc2 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e *e sum* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) ) = sum* y e. X ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
415 nfcv 
 |-  F/_ y ( 1 / ( 2 ^ z ) )
416 nfv 
 |-  F/ y ( ph /\ f : X -1-1-> NN )
417 oveq2 
 |-  ( z = ( f ` y ) -> ( 2 ^ z ) = ( 2 ^ ( f ` y ) ) )
418 417 oveq2d 
 |-  ( z = ( f ` y ) -> ( 1 / ( 2 ^ z ) ) = ( 1 / ( 2 ^ ( f ` y ) ) ) )
419 15 adantr 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> X e. _V )
420 df-f1 
 |-  ( f : X -1-1-> NN <-> ( f : X --> NN /\ Fun `' f ) )
421 420 simprbi 
 |-  ( f : X -1-1-> NN -> Fun `' f )
422 57 feqmptd 
 |-  ( f : X -1-1-> NN -> f = ( y e. X |-> ( f ` y ) ) )
423 422 cnveqd 
 |-  ( f : X -1-1-> NN -> `' f = `' ( y e. X |-> ( f ` y ) ) )
424 423 funeqd 
 |-  ( f : X -1-1-> NN -> ( Fun `' f <-> Fun `' ( y e. X |-> ( f ` y ) ) ) )
425 421 424 mpbid 
 |-  ( f : X -1-1-> NN -> Fun `' ( y e. X |-> ( f ` y ) ) )
426 425 adantl 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> Fun `' ( y e. X |-> ( f ` y ) ) )
427 415 416 25 418 419 426 410 59 esumc 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) = sum* z e. { x | E. y e. X x = ( f ` y ) } ( 1 / ( 2 ^ z ) ) )
428 ffn 
 |-  ( f : X --> NN -> f Fn X )
429 fnrnfv 
 |-  ( f Fn X -> ran f = { x | E. y e. X x = ( f ` y ) } )
430 58 428 429 3syl 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> ran f = { x | E. y e. X x = ( f ` y ) } )
431 364 430 esumeq1d 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) = sum* z e. { x | E. y e. X x = ( f ` y ) } ( 1 / ( 2 ^ z ) ) )
432 427 431 eqtr4d 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) = sum* z e. ran f ( 1 / ( 2 ^ z ) ) )
433 432 adantr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) = sum* z e. ran f ( 1 / ( 2 ^ z ) ) )
434 433 oveq2d 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e *e sum* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) ) = ( e *e sum* z e. ran f ( 1 / ( 2 ^ z ) ) ) )
435 408 414 434 3eqtr2rd 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e *e sum* z e. ran f ( 1 / ( 2 ^ z ) ) ) = sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) )
436 363 simpld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. RR* )
437 xmulrid 
 |-  ( e e. RR* -> ( e *e 1 ) = e )
438 436 437 syl 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e *e 1 ) = e )
439 392 435 438 3brtr3d 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) <_ e )
440 153 339 188 439 syl21anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) <_ e )
441 xleadd2a 
 |-  ( ( ( sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. RR* /\ e e. RR* /\ sum* y e. X ( M ` A ) e. RR* ) /\ sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) <_ e ) -> ( sum* y e. X ( M ` A ) +e sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) ) <_ ( sum* y e. X ( M ` A ) +e e ) )
442 338 189 187 440 441 syl31anc 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( sum* y e. X ( M ` A ) +e sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) ) <_ ( sum* y e. X ( M ` A ) +e e ) )
443 334 442 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) <_ ( sum* y e. X ( M ` A ) +e e ) )
444 286 305 190 332 443 xrletrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* y e. X sum* w e. ( g ` y ) ( R ` w ) <_ ( sum* y e. X ( M ` A ) +e e ) )
445 185 286 190 298 444 xrletrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> sum* c e. U. ran g ( R ` c ) <_ ( sum* y e. X ( M ` A ) +e e ) )
446 161 185 190 259 445 xrletrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) +e e ) )
447 188 rpred 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> e e. RR )
448 186 447 rexaddd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( sum* y e. X ( M ` A ) +e e ) = ( sum* y e. X ( M ` A ) + e ) )
449 446 448 breqtrd 
 |-  ( ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) )
450 449 anasss 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ ( g : X --> { z e. ~P dom R | z ~<_ _om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) )
451 152 450 exlimddv 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) )
452 451 ralrimiva 
 |-  ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) -> A. e e. RR+ ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) )
453 xralrple 
 |-  ( ( ( M ` U_ y e. X A ) e. RR* /\ sum* y e. X ( M ` A ) e. RR ) -> ( ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) <-> A. e e. RR+ ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) ) )
454 160 453 sylan 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> ( ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) <-> A. e e. RR+ ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) ) )
455 454 adantr 
 |-  ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) -> ( ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) <-> A. e e. RR+ ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) ) )
456 452 455 mpbird 
 |-  ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )
457 12 456 exlimddv 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )
458 160 adantr 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) e. RR* )
459 458 pnfged 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ +oo )
460 49 ralrimiva 
 |-  ( ph -> A. y e. X ( M ` A ) e. ( 0 [,] +oo ) )
461 25 esumcl 
 |-  ( ( X e. _V /\ A. y e. X ( M ` A ) e. ( 0 [,] +oo ) ) -> sum* y e. X ( M ` A ) e. ( 0 [,] +oo ) )
462 15 460 461 syl2anc 
 |-  ( ph -> sum* y e. X ( M ` A ) e. ( 0 [,] +oo ) )
463 xrge0nre 
 |-  ( ( sum* y e. X ( M ` A ) e. ( 0 [,] +oo ) /\ -. sum* y e. X ( M ` A ) e. RR ) -> sum* y e. X ( M ` A ) = +oo )
464 462 463 sylan 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> sum* y e. X ( M ` A ) = +oo )
465 459 464 breqtrrd 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )
466 457 465 pm2.61dan 
 |-  ( ph -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )