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)

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 6 ensymi 
 |-  _om ~~ NN
8 domentr 
 |-  ( ( X ~<_ _om /\ _om ~~ NN ) -> X ~<_ NN )
9 5 7 8 sylancl 
 |-  ( 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 nfv 
 |-  F/ y ph
18 nfcv 
 |-  F/_ y X
19 18 nfesum1 
 |-  F/_ y sum* y e. X ( M ` A )
20 nfcv 
 |-  F/_ y RR
21 19 20 nfel 
 |-  F/ y sum* y e. X ( M ` A ) e. RR
22 17 21 nfan 
 |-  F/ y ( ph /\ sum* y e. X ( M ` A ) e. RR )
23 nfv 
 |-  F/ y f : X -1-1-> NN
24 22 23 nfan 
 |-  F/ y ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN )
25 nfv 
 |-  F/ y e e. RR+
26 24 25 nfan 
 |-  F/ y ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ )
27 13 adantr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ph )
28 simpr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> y e. X )
29 15 adantr 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> X e. _V )
30 omsf 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
31 1 feq1i 
 |-  ( M : ~P U. dom R --> ( 0 [,] +oo ) <-> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
32 30 31 sylibr 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
33 2 3 32 syl2anc 
 |-  ( ph -> M : ~P U. dom R --> ( 0 [,] +oo ) )
34 33 adantr 
 |-  ( ( ph /\ y e. X ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
35 3 fdmd 
 |-  ( ph -> dom R = Q )
36 35 unieqd 
 |-  ( ph -> U. dom R = U. Q )
37 36 adantr 
 |-  ( ( ph /\ y e. X ) -> U. dom R = U. Q )
38 4 37 sseqtrrd 
 |-  ( ( ph /\ y e. X ) -> A C_ U. dom R )
39 2 uniexd 
 |-  ( ph -> U. Q e. _V )
40 39 adantr 
 |-  ( ( ph /\ y e. X ) -> U. Q e. _V )
41 ssexg 
 |-  ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
42 4 40 41 syl2anc 
 |-  ( ( ph /\ y e. X ) -> A e. _V )
43 elpwg 
 |-  ( A e. _V -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
44 42 43 syl 
 |-  ( ( ph /\ y e. X ) -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
45 38 44 mpbird 
 |-  ( ( ph /\ y e. X ) -> A e. ~P U. dom R )
46 34 45 ffvelcdmd 
 |-  ( ( ph /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
47 46 adantlr 
 |-  ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
48 simpr 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> sum* y e. X ( M ` A ) e. RR )
49 22 29 47 48 esumcvgre 
 |-  ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. RR )
50 49 adantlr 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( M ` A ) e. RR )
51 50 adantlr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) e. RR )
52 rpssre 
 |-  RR+ C_ RR
53 simplr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
54 2rp 
 |-  2 e. RR+
55 54 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. RR+ )
56 df-f1 
 |-  ( f : X -1-1-> NN <-> ( f : X --> NN /\ Fun `' f ) )
57 56 simplbi 
 |-  ( 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 55 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 53 62 rpdivcld 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR+ )
64 52 63 sselid 
 |-  ( ( ( ( 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 rexadd 
 |-  ( ( ( M ` A ) e. RR /\ ( e / ( 2 ^ ( f ` y ) ) ) e. RR ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) = ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
67 51 65 66 syl2anc 
 |-  ( ( ( ( ( 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 ) ) ) ) )
68 13 46 sylan 
 |-  ( ( ( ( ( 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 ) )
69 dfrp2 
 |-  RR+ = ( 0 (,) +oo )
70 ioossicc 
 |-  ( 0 (,) +oo ) C_ ( 0 [,] +oo )
71 69 70 eqsstri 
 |-  RR+ C_ ( 0 [,] +oo )
72 71 63 sselid 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
73 72 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 ) )
74 68 73 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 ) )
75 67 74 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 ) )
76 52 53 sselid 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
77 76 adantl3r 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
78 52 61 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
79 78 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
80 79 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 )
81 simplr 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
82 81 rpgt0d 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < e )
83 2re 
 |-  2 e. RR
84 83 a1i 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 2 e. RR )
85 60 adantllr 
 |-  ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
86 85 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 )
87 2pos 
 |-  0 < 2
88 87 a1i 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < 2 )
89 expgt0 
 |-  ( ( 2 e. RR /\ ( f ` y ) e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ ( f ` y ) ) )
90 84 86 88 89 syl3anc 
 |-  ( ( ( ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < ( 2 ^ ( f ` y ) ) )
91 77 80 82 90 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 ) ) ) )
92 65 51 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 ) ) ) ) ) )
93 91 92 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 ) ) ) ) )
94 1 fveq1i 
 |-  ( M ` A ) = ( ( toOMeas ` R ) ` A )
95 2 adantr 
 |-  ( ( ph /\ y e. X ) -> Q e. V )
96 3 adantr 
 |-  ( ( ph /\ y e. X ) -> R : Q --> ( 0 [,] +oo ) )
97 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 ) , < ) )
98 95 96 4 97 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 ) , < ) )
99 94 98 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 ) , < ) )
100 13 99 sylan 
 |-  ( ( ( ( ( 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 ) , < ) )
101 100 eqcomd 
 |-  ( ( ( ( ( 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 ) )
102 101 breq1d 
 |-  ( ( ( ( ( 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 ) ) ) ) <-> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
103 93 102 mpbird 
 |-  ( ( ( ( ( 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 ) ) ) ) )
104 75 103 jca 
 |-  ( ( ( ( ( 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 ) /\ 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 ) ) ) ) ) )
105 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
106 xrltso 
 |-  < Or RR*
107 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
108 105 106 107 mp2 
 |-  < Or ( 0 [,] +oo )
109 biid 
 |-  ( < Or ( 0 [,] +oo ) <-> < Or ( 0 [,] +oo ) )
110 108 109 mpbi 
 |-  < Or ( 0 [,] +oo )
111 110 a1i 
 |-  ( ( ph /\ y e. X ) -> < Or ( 0 [,] +oo ) )
112 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 ) )
113 95 96 45 112 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 ) )
114 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 ) ) )
115 113 114 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 ) ) )
116 111 115 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 ) ) ) ) ) )
117 116 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 ) ) ) ) )
118 27 28 104 117 syl21anc 
 |-  ( ( ( ( ( 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 ) ) ) ) )
119 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 ) )
120 esumex 
 |-  sum* w e. x ( R ` w ) e. _V
121 119 120 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 ) )
122 121 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 ) ) ) ) ) )
123 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 ) ) ) ) ) )
124 122 123 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 ) ) ) ) ) )
125 124 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 ) ) ) ) ) )
126 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 ) ) ) ) ) )
127 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 ) ) ) ) ) )
128 125 126 127 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 ) ) ) ) ) )
129 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 ) ) ) ) ) )
130 idd 
 |-  ( u = sum* w e. x ( R ` w ) -> ( sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> sum* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
131 129 130 sylbid 
 |-  ( 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 ) ) ) ) ) )
132 131 imp 
 |-  ( ( 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 ) ) ) ) )
133 132 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 ) ) ) ) )
134 133 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 ) ) ) ) )
135 128 134 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 ) ) ) ) )
136 118 135 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 ) ) ) ) )
137 simpr 
 |-  ( ( A C_ U. z /\ z ~<_ _om ) -> z ~<_ _om )
138 137 a1i 
 |-  ( z e. ~P dom R -> ( ( A C_ U. z /\ z ~<_ _om ) -> z ~<_ _om ) )
139 138 ss2rabi 
 |-  { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } C_ { z e. ~P dom R | z ~<_ _om }
140 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 ) ) ) ) ) ) )
141 139 140 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 ) ) ) ) ) )
142 unieq 
 |-  ( z = x -> U. z = U. x )
143 142 sseq2d 
 |-  ( z = x -> ( A C_ U. z <-> A C_ U. x ) )
144 breq1 
 |-  ( z = x -> ( z ~<_ _om <-> x ~<_ _om ) )
145 143 144 anbi12d 
 |-  ( z = x -> ( ( A C_ U. z /\ z ~<_ _om ) <-> ( A C_ U. x /\ x ~<_ _om ) ) )
146 145 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 ) ) )
147 146 simprbi 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } -> ( A C_ U. x /\ x ~<_ _om ) )
148 147 simpld 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } -> A C_ U. x )
149 148 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 ) )
150 149 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 ) ) ) ) ) ) )
151 150 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 ) ) ) ) ) ) )
152 141 151 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 ) ) ) ) ) ) )
153 136 152 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 ) ) ) ) ) )
154 153 ex 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
155 26 154 ralrimi 
 |-  ( ( ( ( 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 ) ) ) ) ) )
156 unieq 
 |-  ( x = ( g ` y ) -> U. x = U. ( g ` y ) )
157 156 sseq2d 
 |-  ( x = ( g ` y ) -> ( A C_ U. x <-> A C_ U. ( g ` y ) ) )
158 esumeq1 
 |-  ( x = ( g ` y ) -> sum* w e. x ( R ` w ) = sum* w e. ( g ` y ) ( R ` w ) )
159 158 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 ) ) ) ) ) )
160 157 159 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 ) ) ) ) ) ) )
161 160 ac6sg 
 |-  ( X 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 ) ) ) ) ) ) ) )
162 161 imp 
 |-  ( ( X 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 ) ) ) ) ) ) )
163 16 155 162 syl2anc 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
164 13 ad2antrr 
 |-  ( ( ( ( ( ( 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 )
165 38 ralrimiva 
 |-  ( ph -> A. y e. X A C_ U. dom R )
166 iunss 
 |-  ( U_ y e. X A C_ U. dom R <-> A. y e. X A C_ U. dom R )
167 165 166 sylibr 
 |-  ( ph -> U_ y e. X A C_ U. dom R )
168 42 ralrimiva 
 |-  ( ph -> A. y e. X A e. _V )
169 iunexg 
 |-  ( ( X e. _V /\ A. y e. X A e. _V ) -> U_ y e. X A e. _V )
170 15 168 169 syl2anc 
 |-  ( ph -> U_ y e. X A e. _V )
171 elpwg 
 |-  ( U_ y e. X A e. _V -> ( U_ y e. X A e. ~P U. dom R <-> U_ y e. X A C_ U. dom R ) )
172 170 171 syl 
 |-  ( ph -> ( U_ y e. X A e. ~P U. dom R <-> U_ y e. X A C_ U. dom R ) )
173 167 172 mpbird 
 |-  ( ph -> U_ y e. X A e. ~P U. dom R )
174 33 173 ffvelcdmd 
 |-  ( ph -> ( M ` U_ y e. X A ) e. ( 0 [,] +oo ) )
175 105 174 sselid 
 |-  ( ph -> ( M ` U_ y e. X A ) e. RR* )
176 164 175 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* )
177 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 } )
178 29 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 )
179 177 178 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 )
180 rnexg 
 |-  ( g e. _V -> ran g e. _V )
181 uniexg 
 |-  ( ran g e. _V -> U. ran g e. _V )
182 179 180 181 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 )
183 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 )
184 3 ad2antrr 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ c e. U. ran g ) -> R : Q --> ( 0 [,] +oo ) )
185 frn 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> ran g C_ { z e. ~P dom R | z ~<_ _om } )
186 ssrab2 
 |-  { z e. ~P dom R | z ~<_ _om } C_ ~P dom R
187 185 186 sstrdi 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> ran g C_ ~P dom R )
188 187 unissd 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> U. ran g C_ U. ~P dom R )
189 unipw 
 |-  U. ~P dom R = dom R
190 188 189 sseqtrdi 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> U. ran g C_ dom R )
191 190 adantl 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> U. ran g C_ dom R )
192 35 adantr 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> dom R = Q )
193 191 192 sseqtrd 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> U. ran g C_ Q )
194 193 sselda 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ c e. U. ran g ) -> c e. Q )
195 184 194 ffvelcdmd 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ c e. U. ran g ) -> ( R ` c ) e. ( 0 [,] +oo ) )
196 195 ralrimiva 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
197 183 177 196 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 ) )
198 nfcv 
 |-  F/_ c U. ran g
199 198 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 ) )
200 182 197 199 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 ) )
201 105 200 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* )
202 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 )
203 202 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* )
204 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+ )
205 204 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* )
206 203 205 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* )
207 185 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 } )
208 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 )
209 186 208 mpan2 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } -> ran g C_ ~P dom R )
210 sspwuni 
 |-  ( ran g C_ ~P dom R <-> U. ran g C_ dom R )
211 209 210 sylib 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } -> U. ran g C_ dom R )
212 207 211 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 )
213 ffn 
 |-  ( g : X --> { z e. ~P dom R | z ~<_ _om } -> g Fn X )
214 213 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 )
215 164 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 )
216 fnct 
 |-  ( ( g Fn X /\ X ~<_ _om ) -> g ~<_ _om )
217 rnct 
 |-  ( g ~<_ _om -> ran g ~<_ _om )
218 216 217 syl 
 |-  ( ( g Fn X /\ X ~<_ _om ) -> ran g ~<_ _om )
219 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 } )
220 219 biimpi 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } -> A. w e. ran g w e. { z e. ~P dom R | z ~<_ _om } )
221 breq1 
 |-  ( z = w -> ( z ~<_ _om <-> w ~<_ _om ) )
222 221 elrab 
 |-  ( w e. { z e. ~P dom R | z ~<_ _om } <-> ( w e. ~P dom R /\ w ~<_ _om ) )
223 222 simprbi 
 |-  ( w e. { z e. ~P dom R | z ~<_ _om } -> w ~<_ _om )
224 223 ralimi 
 |-  ( A. w e. ran g w e. { z e. ~P dom R | z ~<_ _om } -> A. w e. ran g w ~<_ _om )
225 220 224 syl 
 |-  ( ran g C_ { z e. ~P dom R | z ~<_ _om } -> A. w e. ran g w ~<_ _om )
226 unictb 
 |-  ( ( ran g ~<_ _om /\ A. w e. ran g w ~<_ _om ) -> U. ran g ~<_ _om )
227 218 225 226 syl2an 
 |-  ( ( ( g Fn X /\ X ~<_ _om ) /\ ran g C_ { z e. ~P dom R | z ~<_ _om } ) -> U. ran g ~<_ _om )
228 214 215 207 227 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 )
229 ctex 
 |-  ( U. ran g ~<_ _om -> U. ran g e. _V )
230 elpwg 
 |-  ( U. ran g e. _V -> ( U. ran g e. ~P dom R <-> U. ran g C_ dom R ) )
231 228 229 230 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 ) )
232 212 231 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 )
233 simpl 
 |-  ( ( A C_ U. ( g ` y ) /\ sum* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A C_ U. ( g ` y ) )
234 233 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 ) )
235 fvssunirn 
 |-  ( g ` y ) C_ U. ran g
236 235 unissi 
 |-  U. ( g ` y ) C_ U. U. ran g
237 sstr 
 |-  ( ( A C_ U. ( g ` y ) /\ U. ( g ` y ) C_ U. U. ran g ) -> A C_ U. U. ran g )
238 236 237 mpan2 
 |-  ( A C_ U. ( g ` y ) -> A C_ U. U. ran g )
239 238 ralimi 
 |-  ( A. y e. X A C_ U. ( g ` y ) -> A. y e. X A C_ U. U. ran g )
240 iunss 
 |-  ( U_ y e. X A C_ U. U. ran g <-> A. y e. X A C_ U. U. ran g )
241 239 240 sylibr 
 |-  ( A. y e. X A C_ U. ( g ` y ) -> U_ y e. X A C_ U. U. ran g )
242 234 241 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 )
243 242 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 )
244 232 243 228 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 ) ) )
245 unieq 
 |-  ( z = U. ran g -> U. z = U. U. ran g )
246 245 sseq2d 
 |-  ( z = U. ran g -> ( U_ y e. X A C_ U. z <-> U_ y e. X A C_ U. U. ran g ) )
247 breq1 
 |-  ( z = U. ran g -> ( z ~<_ _om <-> U. ran g ~<_ _om ) )
248 246 247 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 ) ) )
249 248 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 ) ) )
250 244 249 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 ) } )
251 fveq2 
 |-  ( c = w -> ( R ` c ) = ( R ` w ) )
252 251 cbvesumv 
 |-  sum* c e. U. ran g ( R ` c ) = sum* w e. U. ran g ( R ` w )
253 esumeq1 
 |-  ( x = U. ran g -> sum* w e. x ( R ` w ) = sum* w e. U. ran g ( R ` w ) )
254 253 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 ) )
255 250 252 254 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 ) )
256 esumex 
 |-  sum* c e. U. ran g ( R ` c ) e. _V
257 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 ) )
258 257 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 ) ) )
259 256 258 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 ) )
260 255 259 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 ) ) )
261 110 a1i 
 |-  ( ph -> < Or ( 0 [,] +oo ) )
262 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 ) )
263 2 3 173 262 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 ) )
264 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 ) ) )
265 263 264 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 ) ) )
266 261 265 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 ) , < ) ) )
267 1 fveq1i 
 |-  ( M ` U_ y e. X A ) = ( ( toOMeas ` R ) ` U_ y e. X A )
268 167 36 sseqtrd 
 |-  ( ph -> U_ y e. X A C_ U. Q )
269 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 ) , < ) )
270 2 3 268 269 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 ) , < ) )
271 267 270 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 ) , < ) )
272 271 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 ) , < ) ) )
273 272 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 ) , < ) ) )
274 266 273 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 ) ) )
275 164 260 274 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 ) )
276 biid 
 |-  ( -. sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) <-> -. sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
277 275 276 sylib 
 |-  ( ( ( ( ( ( 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 ) )
278 xrlenlt 
 |-  ( ( ( M ` U_ y e. X A ) e. RR* /\ sum* c e. U. ran g ( R ` c ) e. RR* ) -> ( ( M ` U_ y e. X A ) <_ sum* c e. U. ran g ( R ` c ) <-> -. sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) ) )
279 176 201 278 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 ) ) ) ) ) ) -> ( ( M ` U_ y e. X A ) <_ sum* c e. U. ran g ( R ` c ) <-> -. sum* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) ) )
280 277 279 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 ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ sum* c e. U. ran g ( R ` c ) )
281 nfv 
 |-  F/ y g : X --> { z e. ~P dom R | z ~<_ _om }
282 26 281 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 } )
283 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 ) ) ) ) )
284 282 283 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 ) ) ) ) ) )
285 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 )
286 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 } )
287 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 )
288 3 ad3antrrr 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> R : Q --> ( 0 [,] +oo ) )
289 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 } )
290 simplr 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> y e. X )
291 289 290 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 } )
292 186 291 sselid 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) e. ~P dom R )
293 292 elpwid 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ dom R )
294 288 293 fssdmd 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ Q )
295 simpr 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. ( g ` y ) )
296 294 295 sseldd 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. Q )
297 288 296 ffvelcdmd 
 |-  ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( R ` w ) e. ( 0 [,] +oo ) )
298 297 ralrimiva 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> A. w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
299 fvex 
 |-  ( g ` y ) e. _V
300 nfcv 
 |-  F/_ w ( g ` y )
301 300 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 ) )
302 299 301 mpan 
 |-  ( A. w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) -> sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
303 298 302 syl 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> sum* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
304 285 286 287 303 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 ) )
305 304 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 } ) /\ 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 ) ) )
306 284 305 ralrimi 
 |-  ( ( ( ( ( ( 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 ) )
307 18 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 ) )
308 178 306 307 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 ) )
309 105 308 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* )
310 nfv 
 |-  F/ w ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } )
311 simpr 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> g : X --> { z e. ~P dom R | z ~<_ _om } )
312 fniunfv 
 |-  ( g Fn X -> U_ y e. X ( g ` y ) = U. ran g )
313 311 213 312 3syl 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> U_ y e. X ( g ` y ) = U. ran g )
314 310 313 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 ) )
315 15 adantr 
 |-  ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) -> X e. _V )
316 299 a1i 
 |-  ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ _om } ) /\ y e. X ) -> ( g ` y ) e. _V )
317 315 316 297 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 ) )
318 314 317 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 ) )
319 13 318 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 } ) -> sum* w e. U. ran g ( R ` w ) <_ sum* y e. X sum* w e. ( g ` y ) ( R ` w ) )
320 319 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 ) )
321 252 320 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 ) )
322 285 287 46 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 ) )
323 simplll 
 |-  ( ( ( ( ( ( ( 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 /\ sum* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) )
324 323 287 73 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 ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
325 322 324 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 ) )
326 325 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 } ) /\ 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 ) ) )
327 284 326 ralrimi 
 |-  ( ( ( ( ( ( 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 ) )
328 18 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 ) )
329 178 327 328 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 ) )
330 105 329 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* )
331 215 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 )
332 simp-4l 
 |-  ( ( ( ( ( ( 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 /\ sum* y e. X ( M ` A ) e. RR ) )
333 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 )
334 332 333 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 } ) /\ y e. X ) -> ( M ` A ) e. RR )
335 334 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 )
336 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 )
337 336 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 )
338 id 
 |-  ( 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 ) ) ) ) )
339 338 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 } ) /\ 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 ) ) ) ) )
340 66 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 ) ) ) ) ) )
341 340 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 ) ) ) ) )
342 335 337 339 341 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 ) ) ) ) )
343 342 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 ) ) ) ) ) )
344 332 simpld 
 |-  ( ( ( ( ( ( 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 )
345 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 } )
346 344 345 333 303 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 ) )
347 105 346 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* )
348 334 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* )
349 336 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* )
350 348 349 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* )
351 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 ) ) ) ) ) )
352 347 350 351 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 ) ) ) ) ) )
353 343 352 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 ) ) ) ) ) )
354 353 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 ) ) ) ) ) )
355 354 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 -> ( ( 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 ) ) ) ) ) ) )
356 282 355 ralrimi 
 |-  ( ( ( ( ( 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. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
357 ralim 
 |-  ( 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. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( 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 ) ) ) ) ) )
358 356 357 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 ) ) ) ) ) -> A. y e. X sum* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
359 358 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 ) ) ) ) )
360 359 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 ) ) ) ) )
361 284 18 331 304 325 360 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 ) ) ) ) )
362 164 46 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 ) )
363 284 18 331 362 324 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 ) ) ) ) )
364 324 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 } ) /\ 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 ) ) )
365 284 364 ralrimi 
 |-  ( ( ( ( ( ( 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 ) )
366 18 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 ) )
367 178 365 366 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 ) )
368 105 367 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* )
369 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 )
370 vex 
 |-  f e. _V
371 370 rnex 
 |-  ran f e. _V
372 371 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ran f e. _V )
373 58 frnd 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> ran f C_ NN )
374 373 adantr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ran f C_ NN )
375 374 sselda 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. ran f ) -> z e. NN )
376 54 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> 2 e. RR+ )
377 simpr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> z e. NN )
378 377 nnzd 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> z e. ZZ )
379 376 378 rpexpcld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 2 ^ z ) e. RR+ )
380 379 rpreccld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. RR+ )
381 71 380 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
382 381 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
383 375 382 syldan 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. ran f ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
384 383 ralrimiva 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> A. z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
385 nfcv 
 |-  F/_ z ran f
386 385 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 ) )
387 372 384 386 syl2anc 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
388 105 387 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) e. RR* )
389 1xr 
 |-  1 e. RR*
390 389 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> 1 e. RR* )
391 71 sseli 
 |-  ( e e. RR+ -> e e. ( 0 [,] +oo ) )
392 391 adantl 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. ( 0 [,] +oo ) )
393 elxrge0 
 |-  ( e e. ( 0 [,] +oo ) <-> ( e e. RR* /\ 0 <_ e ) )
394 392 393 sylib 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e e. RR* /\ 0 <_ e ) )
395 nfv 
 |-  F/ z ( ph /\ f : X -1-1-> NN )
396 nnex 
 |-  NN e. _V
397 396 a1i 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> NN e. _V )
398 395 397 381 373 esummono 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) <_ sum* z e. NN ( 1 / ( 2 ^ z ) ) )
399 oveq2 
 |-  ( z = w -> ( 2 ^ z ) = ( 2 ^ w ) )
400 399 oveq2d 
 |-  ( z = w -> ( 1 / ( 2 ^ z ) ) = ( 1 / ( 2 ^ w ) ) )
401 ioossico 
 |-  ( 0 (,) +oo ) C_ ( 0 [,) +oo )
402 69 401 eqsstri 
 |-  RR+ C_ ( 0 [,) +oo )
403 402 380 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,) +oo ) )
404 eqidd 
 |-  ( z e. NN -> ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) = ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) )
405 simpr 
 |-  ( ( z e. NN /\ w = z ) -> w = z )
406 405 oveq2d 
 |-  ( ( z e. NN /\ w = z ) -> ( 2 ^ w ) = ( 2 ^ z ) )
407 406 oveq2d 
 |-  ( ( z e. NN /\ w = z ) -> ( 1 / ( 2 ^ w ) ) = ( 1 / ( 2 ^ z ) ) )
408 id 
 |-  ( z e. NN -> z e. NN )
409 ovexd 
 |-  ( z e. NN -> ( 1 / ( 2 ^ z ) ) e. _V )
410 404 407 408 409 fvmptd 
 |-  ( z e. NN -> ( ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ` z ) = ( 1 / ( 2 ^ z ) ) )
411 410 adantl 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ` z ) = ( 1 / ( 2 ^ z ) ) )
412 ax-1cn 
 |-  1 e. CC
413 eqid 
 |-  ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) = ( w e. NN |-> ( 1 / ( 2 ^ w ) ) )
414 413 geo2lim 
 |-  ( 1 e. CC -> seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1 )
415 412 414 ax-mp 
 |-  seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1
416 415 a1i 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1 )
417 1re 
 |-  1 e. RR
418 417 a1i 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> 1 e. RR )
419 400 403 411 416 418 esumcvgsum 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. NN ( 1 / ( 2 ^ z ) ) = sum_ z e. NN ( 1 / ( 2 ^ z ) ) )
420 geoihalfsum 
 |-  sum_ z e. NN ( 1 / ( 2 ^ z ) ) = 1
421 419 420 eqtrdi 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. NN ( 1 / ( 2 ^ z ) ) = 1 )
422 398 421 breqtrd 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 )
423 422 adantr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 )
424 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 ) )
425 388 390 394 423 424 syl31anc 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e *e sum* z e. ran f ( 1 / ( 2 ^ z ) ) ) <_ ( e *e 1 ) )
426 17 23 nfan 
 |-  F/ y ( ph /\ f : X -1-1-> NN )
427 426 25 nfan 
 |-  F/ y ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ )
428 76 recnd 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. CC )
429 78 recnd 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. CC )
430 429 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. CC )
431 2cn 
 |-  2 e. CC
432 431 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. CC )
433 2ne0 
 |-  2 =/= 0
434 433 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 =/= 0 )
435 432 434 60 expne0d 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) =/= 0 )
436 435 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) =/= 0 )
437 428 430 436 divrecd 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
438 1rp 
 |-  1 e. RR+
439 438 a1i 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 1 e. RR+ )
440 439 61 rpdivcld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR+ )
441 52 440 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR )
442 441 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR )
443 rexmul 
 |-  ( ( e e. RR /\ ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR ) -> ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
444 76 442 443 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 ) ) ) ) )
445 437 444 eqtr4d 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) = ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
446 445 ralrimiva 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> A. y e. X ( e / ( 2 ^ ( f ` y ) ) ) = ( e *e ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
447 427 446 esumeq2d 
 |-  ( ( ( 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 ) ) ) ) )
448 15 ad2antrr 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> X e. _V )
449 71 440 sselid 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
450 449 adantlr 
 |-  ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
451 402 a1i 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> RR+ C_ ( 0 [,) +oo ) )
452 451 sselda 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. ( 0 [,) +oo ) )
453 448 450 452 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 ) ) ) ) )
454 nfcv 
 |-  F/_ y ( 1 / ( 2 ^ z ) )
455 oveq2 
 |-  ( z = ( f ` y ) -> ( 2 ^ z ) = ( 2 ^ ( f ` y ) ) )
456 455 oveq2d 
 |-  ( z = ( f ` y ) -> ( 1 / ( 2 ^ z ) ) = ( 1 / ( 2 ^ ( f ` y ) ) ) )
457 15 adantr 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> X e. _V )
458 56 simprbi 
 |-  ( f : X -1-1-> NN -> Fun `' f )
459 57 feqmptd 
 |-  ( f : X -1-1-> NN -> f = ( y e. X |-> ( f ` y ) ) )
460 459 cnveqd 
 |-  ( f : X -1-1-> NN -> `' f = `' ( y e. X |-> ( f ` y ) ) )
461 460 funeqd 
 |-  ( f : X -1-1-> NN -> ( Fun `' f <-> Fun `' ( y e. X |-> ( f ` y ) ) ) )
462 458 461 mpbid 
 |-  ( f : X -1-1-> NN -> Fun `' ( y e. X |-> ( f ` y ) ) )
463 462 adantl 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> Fun `' ( y e. X |-> ( f ` y ) ) )
464 454 426 18 456 457 463 449 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 ) ) )
465 ffn 
 |-  ( f : X --> NN -> f Fn X )
466 fnrnfv 
 |-  ( f Fn X -> ran f = { x | E. y e. X x = ( f ` y ) } )
467 58 465 466 3syl 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> ran f = { x | E. y e. X x = ( f ` y ) } )
468 395 467 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 ) ) )
469 464 468 eqtr4d 
 |-  ( ( ph /\ f : X -1-1-> NN ) -> sum* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) = sum* z e. ran f ( 1 / ( 2 ^ z ) ) )
470 469 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 ) ) )
471 470 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 ) ) ) )
472 447 453 471 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 ) ) ) )
473 394 simpld 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. RR* )
474 xmulrid 
 |-  ( e e. RR* -> ( e *e 1 ) = e )
475 473 474 syl 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e *e 1 ) = e )
476 425 472 475 3brtr3d 
 |-  ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> sum* y e. X ( e / ( 2 ^ ( f ` y ) ) ) <_ e )
477 164 369 204 476 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 )
478 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 ) )
479 368 205 203 477 478 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 ) )
480 363 479 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 ) )
481 309 330 206 361 480 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 ) )
482 201 309 206 321 481 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 ) )
483 176 201 206 280 482 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 ) )
484 204 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 )
485 rexadd 
 |-  ( ( sum* y e. X ( M ` A ) e. RR /\ e e. RR ) -> ( sum* y e. X ( M ` A ) +e e ) = ( sum* y e. X ( M ` A ) + e ) )
486 202 484 485 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 ) = ( sum* y e. X ( M ` A ) + e ) )
487 483 486 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 ) )
488 487 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 ) )
489 488 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 } /\ 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 ) ) )
490 489 exlimdv 
 |-  ( ( ( ( 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 ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ ( sum* y e. X ( M ` A ) + e ) ) )
491 163 490 mpd 
 |-  ( ( ( ( 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 ) )
492 491 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 ) )
493 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 ) ) )
494 175 493 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 ) ) )
495 494 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 ) ) )
496 492 495 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 ) )
497 496 ex 
 |-  ( ( 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 ) ) )
498 497 exlimdv 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> ( E. f f : X -1-1-> NN -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) ) )
499 12 498 mpd 
 |-  ( ( ph /\ sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )
500 175 adantr 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) e. RR* )
501 pnfge 
 |-  ( ( M ` U_ y e. X A ) e. RR* -> ( M ` U_ y e. X A ) <_ +oo )
502 500 501 syl 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ +oo )
503 46 ralrimiva 
 |-  ( ph -> A. y e. X ( M ` A ) e. ( 0 [,] +oo ) )
504 18 esumcl 
 |-  ( ( X e. _V /\ A. y e. X ( M ` A ) e. ( 0 [,] +oo ) ) -> sum* y e. X ( M ` A ) e. ( 0 [,] +oo ) )
505 15 503 504 syl2anc 
 |-  ( ph -> sum* y e. X ( M ` A ) e. ( 0 [,] +oo ) )
506 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 )
507 505 506 sylan 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> sum* y e. X ( M ` A ) = +oo )
508 502 507 breqtrrd 
 |-  ( ( ph /\ -. sum* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )
509 499 508 pm2.61dan 
 |-  ( ph -> ( M ` U_ y e. X A ) <_ sum* y e. X ( M ` A ) )