Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  omssubadd Structured version   Visualization version   Unicode version

Theorem omssubadd 29201
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.)
Hypotheses
Ref Expression
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
Ref Expression
omssubadd  |-  ( ph  ->  ( M `  U_ y  e.  X  A )  <_ Σ* y  e.  X ( M `
 A ) )
Distinct variable groups:    y, Q    y, R    y, V    ph, y    y, X
Allowed substitution hints:    A( y)    M( y)

Proof of Theorem omssubadd
Dummy variables  x  z  e  t  u  w  f  g  h  v  c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omssubadd.b . . . . . 6  |-  ( ph  ->  X  ~<_  om )
2 nnenom 12231 . . . . . . 7  |-  NN  ~~  om
32ensymi 7637 . . . . . 6  |-  om  ~~  NN
4 domentr 7646 . . . . . 6  |-  ( ( X  ~<_  om  /\  om  ~~  NN )  ->  X  ~<_  NN )
51, 3, 4sylancl 675 . . . . 5  |-  ( ph  ->  X  ~<_  NN )
6 brdomi 7598 . . . . 5  |-  ( X  ~<_  NN  ->  E. f 
f : X -1-1-> NN )
75, 6syl 17 . . . 4  |-  ( ph  ->  E. f  f : X -1-1-> NN )
87adantr 472 . . 3  |-  ( (
ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  ->  E. f  f : X -1-1-> NN )
9 simplll 776 . . . . . . . . . 10  |-  ( ( ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  ->  ph )
10 ctex 7602 . . . . . . . . . . 11  |-  ( X  ~<_  om  ->  X  e.  _V )
111, 10syl 17 . . . . . . . . . 10  |-  ( ph  ->  X  e.  _V )
129, 11syl 17 . . . . . . . . 9  |-  ( ( ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  ->  X  e. 
_V )
13 nfv 1769 . . . . . . . . . . . . 13  |-  F/ y
ph
14 nfcv 2612 . . . . . . . . . . . . . . 15  |-  F/_ y X
1514nfesum1 28935 . . . . . . . . . . . . . 14  |-  F/_ yΣ* y  e.  X ( M `  A )
16 nfcv 2612 . . . . . . . . . . . . . 14  |-  F/_ y RR
1715, 16nfel 2624 . . . . . . . . . . . . 13  |-  F/ yΣ* y  e.  X ( M `
 A )  e.  RR
1813, 17nfan 2031 . . . . . . . . . . . 12  |-  F/ y ( ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )
19 nfv 1769 . . . . . . . . . . . 12  |-  F/ y  f : X -1-1-> NN
2018, 19nfan 2031 . . . . . . . . . . 11  |-  F/ y ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )
21 nfv 1769 . . . . . . . . . . 11  |-  F/ y  e  e.  RR+
2220, 21nfan 2031 . . . . . . . . . 10  |-  F/ y ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )
239adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  ph )
24 simpr 468 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  y  e.  X )
2511adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  ->  X  e.  _V )
26 oms.o . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  Q  e.  V )
27 oms.r . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  R : Q --> ( 0 [,] +oo ) )
28 omsf 29193 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Q  e.  V  /\  R : Q --> ( 0 [,] +oo ) )  ->  (toOMeas `  R ) : ~P U. dom  R --> ( 0 [,] +oo ) )
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  M  =  (toOMeas `  R )
3029feq1i 5730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M : ~P U. dom  R --> ( 0 [,] +oo ) 
<->  (toOMeas `  R ) : ~P U. dom  R --> ( 0 [,] +oo ) )
3128, 30sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Q  e.  V  /\  R : Q --> ( 0 [,] +oo ) )  ->  M : ~P U.
dom  R --> ( 0 [,] +oo ) )
3226, 27, 31syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  M : ~P U. dom  R --> ( 0 [,] +oo ) )
3332adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  X )  ->  M : ~P U. dom  R --> ( 0 [,] +oo ) )
34 omssubadd.a . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  X )  ->  A  C_ 
U. Q )
35 fdm 5745 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( R : Q --> ( 0 [,] +oo )  ->  dom  R  =  Q )
3627, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  dom  R  =  Q )
3736unieqd 4200 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  U. dom  R  = 
U. Q )
3837adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  X )  ->  U. dom  R  =  U. Q )
3934, 38sseqtr4d 3455 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  X )  ->  A  C_ 
U. dom  R )
40 uniexg 6607 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Q  e.  V  ->  U. Q  e.  _V )
4126, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  U. Q  e.  _V )
4241adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  X )  ->  U. Q  e.  _V )
43 ssexg 4542 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  C_  U. Q  /\  U. Q  e.  _V )  ->  A  e.  _V )
4434, 42, 43syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  X )  ->  A  e.  _V )
45 elpwg 3950 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A  e.  _V  ->  ( A  e.  ~P U. dom  R  <-> 
A  C_  U. dom  R
) )
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  X )  ->  ( A  e.  ~P U. dom  R  <-> 
A  C_  U. dom  R
) )
4739, 46mpbird 240 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  X )  ->  A  e.  ~P U. dom  R
)
4833, 47ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  X )  ->  ( M `  A )  e.  ( 0 [,] +oo ) )
4948adantlr 729 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  /\  y  e.  X
)  ->  ( M `  A )  e.  ( 0 [,] +oo )
)
50 simpr 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  -> Σ* y  e.  X ( M `  A )  e.  RR )
5118, 25, 49, 50esumcvgre 28986 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  /\  y  e.  X
)  ->  ( M `  A )  e.  RR )
5251adantlr 729 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  ( M `  A )  e.  RR )
5352adantlr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  ( M `  A )  e.  RR )
54 rpssre 11335 . . . . . . . . . . . . . . . . . . 19  |-  RR+  C_  RR
55 simplr 770 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  e  e.  RR+ )
56 2rp 11330 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  RR+
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  2  e.  RR+ )
58 df-f1 5594 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : X -1-1-> NN  <->  ( f : X --> NN  /\  Fun  `' f ) )
5958simplbi 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f : X -1-1-> NN  ->  f : X --> NN )
6059adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  f : X -1-1-> NN )  ->  f : X --> NN )
6160ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
f `  y )  e.  NN )
6261nnzd 11062 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
f `  y )  e.  ZZ )
6357, 62rpexpcld 12477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
2 ^ ( f `
 y ) )  e.  RR+ )
6463adantlr 729 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( 2 ^ ( f `  y ) )  e.  RR+ )
6555, 64rpdivcld 11381 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( e  /  ( 2 ^ ( f `  y
) ) )  e.  RR+ )
6654, 65sseldi 3416 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( e  /  ( 2 ^ ( f `  y
) ) )  e.  RR )
6766adantl3r 764 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  (
e  /  ( 2 ^ ( f `  y ) ) )  e.  RR )
68 rexadd 11548 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M `  A
)  e.  RR  /\  ( e  /  (
2 ^ ( f `
 y ) ) )  e.  RR )  ->  ( ( M `
 A ) +e ( e  / 
( 2 ^ (
f `  y )
) ) )  =  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) )
6953, 67, 68syl2anc 673 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ Σ* 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 )
) ) ) )
709, 48sylan 479 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  ( M `  A )  e.  ( 0 [,] +oo ) )
71 dfrp2 28427 . . . . . . . . . . . . . . . . . . . 20  |-  RR+  =  ( 0 (,) +oo )
72 ioossicc 11745 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) +oo )  C_  ( 0 [,] +oo )
7371, 72eqsstri 3448 . . . . . . . . . . . . . . . . . . 19  |-  RR+  C_  (
0 [,] +oo )
7473, 65sseldi 3416 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( e  /  ( 2 ^ ( f `  y
) ) )  e.  ( 0 [,] +oo ) )
7574adantl3r 764 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ Σ* 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 ) )
7670, 75xrge0addcld 28419 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ Σ* 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 ) )
7769, 76eqeltrrd 2550 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\ Σ* 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 ) )
7854, 55sseldi 3416 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  e  e.  RR )
7978adantl3r 764 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  e  e.  RR )
8054, 63sseldi 3416 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
2 ^ ( f `
 y ) )  e.  RR )
8180adantlr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( 2 ^ ( f `  y ) )  e.  RR )
8281adantl3r 764 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  (
2 ^ ( f `
 y ) )  e.  RR )
83 simplr 770 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  e  e.  RR+ )
8483rpgt0d 11367 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  0  <  e )
85 2re 10701 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
8685a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  2  e.  RR )
8762adantllr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
f `  y )  e.  ZZ )
8887adantlr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  (
f `  y )  e.  ZZ )
89 2pos 10723 . . . . . . . . . . . . . . . . . . . 20  |-  0  <  2
9089a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  0  <  2 )
91 expgt0 12343 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  e.  RR  /\  ( f `  y
)  e.  ZZ  /\  0  <  2 )  -> 
0  <  ( 2 ^ ( f `  y ) ) )
9286, 88, 90, 91syl3anc 1292 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  0  <  ( 2 ^ (
f `  y )
) )
9379, 82, 84, 92divgt0d 10564 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  0  <  ( e  /  (
2 ^ ( f `
 y ) ) ) )
9467, 53ltaddposd 10218 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ Σ* 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
) ) ) ) ) )
9593, 94mpbid 215 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ Σ* 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 ) ) ) ) )
9629fveq1i 5880 . . . . . . . . . . . . . . . . . . . 20  |-  ( M `
 A )  =  ( (toOMeas `  R
) `  A )
9726adantr 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  X )  ->  Q  e.  V )
9827adantr 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  X )  ->  R : Q --> ( 0 [,] +oo ) )
99 omsfval 29191 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) }  |-> Σ*
w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) )
10097, 98, 34, 99syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  X )  ->  (
(toOMeas `  R ) `  A )  = inf ( ran  ( x  e.  {
z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  <  ) )
10196, 100syl5eq 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  X )  ->  ( M `  A )  = inf ( ran  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ*
w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) )
1029, 101sylan 479 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  |-> Σ*
w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) )
103102eqcomd 2477 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  <  )  =  ( M `  A ) )
104103breq1d 4405 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  <  )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) )  <-> 
( M `  A
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) )
10595, 104mpbird 240 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  <  )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) )
10677, 105jca 541 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  <  )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) ) )
107 iccssxr 11742 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] +oo )  C_  RR*
108 xrltso 11463 . . . . . . . . . . . . . . . . . . 19  |-  <  Or  RR*
109 soss 4778 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] +oo )  C_ 
RR*  ->  (  <  Or  RR* 
->  <  Or  ( 0 [,] +oo ) ) )
110107, 108, 109mp2 9 . . . . . . . . . . . . . . . . . 18  |-  <  Or  ( 0 [,] +oo )
111 biid 244 . . . . . . . . . . . . . . . . . 18  |-  (  < 
Or  ( 0 [,] +oo )  <->  <  Or  ( 0 [,] +oo ) )
112110, 111mpbi 213 . . . . . . . . . . . . . . . . 17  |-  <  Or  ( 0 [,] +oo )
113112a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  X )  ->  <  Or  ( 0 [,] +oo ) )
114 omscl 29192 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) }  |-> Σ*
w  e.  x ( R `  w ) )  C_  ( 0 [,] +oo ) )
11597, 98, 47, 114syl3anc 1292 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  X )  ->  ran  ( x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  C_  (
0 [,] +oo )
)
116 xrge0infss 28415 . . . . . . . . . . . . . . . . 17  |-  ( ran  ( x  e.  {
z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* 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 ) }  |-> Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) u  < 
h ) ) )
117115, 116syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) }  |-> Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) u  < 
h ) ) )
118113, 117infglb 8024 . . . . . . . . . . . . . . 15  |-  ( (
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 ) }  |-> Σ*
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 ) }  |-> Σ* w  e.  x
( R `  w
) ) u  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )
119118imp 436 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) }  |-> Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) u  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) )
12023, 24, 106, 119syl21anc 1291 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) u  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) )
121 eqid 2471 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ*
w  e.  x ( R `  w ) )  =  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ*
w  e.  x ( R `  w ) )
122 esumex 28924 . . . . . . . . . . . . . . . . . . 19  |- Σ* w  e.  x
( R `  w
)  e.  _V
123121, 122elrnmpti 5091 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  ran  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ*
w  e.  x ( R `  w ) )  <->  E. x  e.  {
z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) } u  = Σ* w  e.  x ( R `
 w ) )
124123anbi1i 709 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* 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  = Σ* w  e.  x
( R `  w
)  /\  u  <  ( ( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) ) )
125 r19.41v 2928 . . . . . . . . . . . . . . . . 17  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  ( u  = Σ* 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  = Σ* w  e.  x ( R `
 w )  /\  u  <  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) ) )
126124, 125bitr4i 260 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* 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  = Σ* w  e.  x ( R `  w )  /\  u  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) ) )
127126exbii 1726 . . . . . . . . . . . . . . 15  |-  ( E. u ( u  e. 
ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* 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  = Σ* w  e.  x ( R `  w )  /\  u  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) ) )
128 df-rex 2762 . . . . . . . . . . . . . . 15  |-  ( E. u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* 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 ) }  |-> Σ*
w  e.  x ( R `  w ) )  /\  u  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )
129 rexcom4 3053 . . . . . . . . . . . . . . 15  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) } E. u
( u  = Σ* 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  = Σ* w  e.  x ( R `  w )  /\  u  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) ) )
130127, 128, 1293bitr4i 285 . . . . . . . . . . . . . 14  |-  ( E. u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* 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  = Σ* w  e.  x ( R `  w )  /\  u  <  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )
131 breq1 4398 . . . . . . . . . . . . . . . . . 18  |-  ( u  = Σ* w  e.  x ( R `  w )  ->  ( u  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) )  <-> Σ* w  e.  x ( R `  w )  <  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )
132 idd 24 . . . . . . . . . . . . . . . . . 18  |-  ( u  = Σ* w  e.  x ( R `  w )  ->  (Σ* w  e.  x ( R `  w )  <  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) )  -> Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) )
133131, 132sylbid 223 . . . . . . . . . . . . . . . . 17  |-  ( u  = Σ* w  e.  x ( R `  w )  ->  ( u  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) )  -> Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) )
134133imp 436 . . . . . . . . . . . . . . . 16  |-  ( ( u  = Σ* w  e.  x
( R `  w
)  /\  u  <  ( ( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) )  -> Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) )
135134exlimiv 1784 . . . . . . . . . . . . . . 15  |-  ( E. u ( u  = Σ* w  e.  x ( R `
 w )  /\  u  <  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) )  -> Σ* w  e.  x ( R `  w )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) )
136135reximi 2852 . . . . . . . . . . . . . 14  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) } E. u
( u  = Σ* 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 ) }Σ* w  e.  x ( R `  w )  <  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) )
137130, 136sylbi 200 . . . . . . . . . . . . 13  |-  ( E. u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* 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 ) }Σ* w  e.  x ( R `  w )  <  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) )
138120, 137syl 17 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }Σ* w  e.  x ( R `  w )  <  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) )
139 simpr 468 . . . . . . . . . . . . . . . 16  |-  ( ( A  C_  U. z  /\  z  ~<_  om )  ->  z  ~<_  om )
140139a1i 11 . . . . . . . . . . . . . . 15  |-  ( z  e.  ~P dom  R  ->  ( ( A  C_  U. z  /\  z  ~<_  om )  ->  z  ~<_  om )
)
141140ss2rabi 3497 . . . . . . . . . . . . . 14  |-  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  C_  { z  e.  ~P dom  R  |  z  ~<_  om }
142 rexss 3482 . . . . . . . . . . . . . 14  |-  ( { 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 ) }Σ* 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 ) }  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) )
143141, 142ax-mp 5 . . . . . . . . . . . . 13  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }Σ* 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 ) }  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) )
144 unieq 4198 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  x  ->  U. z  =  U. x )
145144sseq2d 3446 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  x  ->  ( A  C_  U. z  <->  A  C_  U. x
) )
146 breq1 4398 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  x  ->  (
z  ~<_  om  <->  x  ~<_  om )
)
147145, 146anbi12d 725 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  x  ->  (
( A  C_  U. z  /\  z  ~<_  om )  <->  ( A  C_  U. x  /\  x  ~<_  om )
) )
148147elrab 3184 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) } 
<->  ( x  e.  ~P dom  R  /\  ( A 
C_  U. x  /\  x  ~<_  om ) ) )
149148simprbi 471 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  ->  ( A  C_  U. x  /\  x  ~<_  om ) )
150149simpld 466 . . . . . . . . . . . . . . . 16  |-  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  ->  A  C_  U. x
)
151150a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\ Σ* 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 ) )
152151anim1d 574 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) )  ->  ( A  C_  U. x  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) )
153152reximdv 2857 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }  /\ Σ* 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  /\ Σ* w  e.  x ( R `  w )  <  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) ) )
154143, 153syl5bi 225 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ Σ* 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 ) }Σ* 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  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) )
155138, 154mpd 15 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\ Σ* 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  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) )
156155ex 441 . . . . . . . . . 10  |-  ( ( ( ( ph  /\ Σ* 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  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) )
15722, 156ralrimi 2800 . . . . . . . . 9  |-  ( ( ( ( ph  /\ Σ* 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  /\ Σ* w  e.  x
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) )
158 unieq 4198 . . . . . . . . . . . . 13  |-  ( x  =  ( g `  y )  ->  U. x  =  U. ( g `  y ) )
159158sseq2d 3446 . . . . . . . . . . . 12  |-  ( x  =  ( g `  y )  ->  ( A  C_  U. x  <->  A  C_  U. (
g `  y )
) )
160 esumeq1 28929 . . . . . . . . . . . . 13  |-  ( x  =  ( g `  y )  -> Σ* w  e.  x
( R `  w
)  = Σ* w  e.  (
g `  y )
( R `  w
) )
161160breq1d 4405 . . . . . . . . . . . 12  |-  ( x  =  ( g `  y )  ->  (Σ* w  e.  x ( R `  w )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) )  <-> Σ* w  e.  ( g `  y
) ( R `  w )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) ) )
162159, 161anbi12d 725 . . . . . . . . . . 11  |-  ( x  =  ( g `  y )  ->  (
( A  C_  U. x  /\ Σ* w  e.  x ( R `  w )  <  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) )  <->  ( A  C_ 
U. ( g `  y )  /\ Σ* w  e.  (
g `  y )
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) )
163162ac6sg 8936 . . . . . . . . . 10  |-  ( X  e.  _V  ->  ( A. y  e.  X  E. x  e.  { z  e.  ~P dom  R  |  z  ~<_  om }  ( A  C_  U. x  /\ Σ* 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 )  /\ Σ* w  e.  (
g `  y )
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) ) )
164163imp 436 . . . . . . . . 9  |-  ( ( X  e.  _V  /\  A. y  e.  X  E. x  e.  { z  e.  ~P dom  R  | 
z  ~<_  om }  ( A 
C_  U. x  /\ Σ* 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 )  /\ Σ* w  e.  (
g `  y )
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) )
16512, 157, 164syl2anc 673 . . . . . . . 8  |-  ( ( ( ( ph  /\ Σ* 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 )  /\ Σ* w  e.  (
g `  y )
( R `  w
)  <  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) ) ) )
1669ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  ph )
16739ralrimiva 2809 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. y  e.  X  A  C_  U. dom  R
)
168 iunss 4310 . . . . . . . . . . . . . . . . . 18  |-  ( U_ y  e.  X  A  C_ 
U. dom  R  <->  A. y  e.  X  A  C_  U. dom  R )
169167, 168sylibr 217 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  U_ y  e.  X  A  C_  U. dom  R
)
17044ralrimiva 2809 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. y  e.  X  A  e.  _V )
171 iunexg 6788 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X  e.  _V  /\  A. y  e.  X  A  e.  _V )  ->  U_ y  e.  X  A  e.  _V )
17211, 170, 171syl2anc 673 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U_ y  e.  X  A  e.  _V )
173 elpwg 3950 . . . . . . . . . . . . . . . . . 18  |-  ( 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 )
)
174172, 173syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U_ y  e.  X  A  e.  ~P U.
dom  R  <->  U_ y  e.  X  A  C_  U. dom  R
) )
175169, 174mpbird 240 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  U_ y  e.  X  A  e.  ~P U. dom  R )
17632, 175ffvelrnd 6038 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( M `  U_ y  e.  X  A )  e.  ( 0 [,] +oo ) )
177107, 176sseldi 3416 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M `  U_ y  e.  X  A )  e.  RR* )
178166, 177syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
( M `  U_ y  e.  X  A )  e.  RR* )
179 simplr 770 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )
18025ad4antr 746 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  X  e.  _V )
181 fex 6155 . . . . . . . . . . . . . . . . 17  |-  ( ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  /\  X  e.  _V )  ->  g  e.  _V )
182179, 180, 181syl2anc 673 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
g  e.  _V )
183 rnexg 6744 . . . . . . . . . . . . . . . 16  |-  ( g  e.  _V  ->  ran  g  e.  _V )
184 uniexg 6607 . . . . . . . . . . . . . . . 16  |-  ( ran  g  e.  _V  ->  U.
ran  g  e.  _V )
185182, 183, 1843syl 18 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  U. ran  g  e.  _V )
186 simp-5l 786 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  ph )
18727ad2antrr 740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  c  e.  U. ran  g
)  ->  R : Q
--> ( 0 [,] +oo ) )
188 frn 5747 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om } )
189 ssrab2 3500 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  e.  ~P dom  R  |  z  ~<_  om }  C_  ~P dom  R
190188, 189syl6ss 3430 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  ran  g  C_  ~P dom  R )
191190unissd 4214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  U.
ran  g  C_  U. ~P dom  R )
192 unipw 4650 . . . . . . . . . . . . . . . . . . . . . 22  |-  U. ~P dom  R  =  dom  R
193191, 192syl6sseq 3464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  U.
ran  g  C_  dom  R )
194193adantl 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  U. ran  g  C_  dom  R )
19536adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  dom  R  =  Q )
196194, 195sseqtrd 3454 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  U. ran  g  C_  Q )
197196sselda 3418 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  c  e.  U. ran  g
)  ->  c  e.  Q )
198187, 197ffvelrnd 6038 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  c  e.  U. ran  g
)  ->  ( R `  c )  e.  ( 0 [,] +oo )
)
199198ralrimiva 2809 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  A. c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo ) )
200186, 179, 199syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  A. c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo )
)
201 nfcv 2612 . . . . . . . . . . . . . . . 16  |-  F/_ c U. ran  g
202201esumcl 28925 . . . . . . . . . . . . . . 15  |-  ( ( U. ran  g  e. 
_V  /\  A. c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo ) )  -> Σ* c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo )
)
203185, 200, 202syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> Σ* c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo ) )
204107, 203sseldi 3416 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> Σ* c  e.  U. ran  g ( R `  c )  e.  RR* )
205 simp-5r 787 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> Σ* y  e.  X ( M `  A )  e.  RR )
206205rexrd 9708 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> Σ* y  e.  X ( M `  A )  e.  RR* )
207 simpllr 777 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
e  e.  RR+ )
208207rpxrd 11365 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
e  e.  RR* )
209206, 208xaddcld 11612 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
(Σ* y  e.  X ( M `  A ) +e e )  e.  RR* )
210188ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  ran  g  C_  { z  e.  ~P dom  R  |  z  ~<_  om } )
211 sstr 3426 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 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 )
212189, 211mpan2 685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  ->  ran  g  C_  ~P dom  R
)
213 sspwuni 4360 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ran  g  C_  ~P dom  R  <->  U. ran  g  C_  dom  R )
214212, 213sylib 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  ->  U. ran  g  C_  dom  R )
215210, 214syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  U. ran  g  C_  dom  R )
216 ffn 5739 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  g  Fn  X )
217216ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
g  Fn  X )
218166, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  X  ~<_  om )
219 fnct 28372 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g  Fn  X  /\  X  ~<_  om )  ->  g  ~<_  om )
220 rnct 28375 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g  ~<_  om  ->  ran  g  ~<_  om )
221219, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  Fn  X  /\  X  ~<_  om )  ->  ran  g  ~<_  om )
222 dfss3 3408 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  <->  A. w  e.  ran  g  w  e. 
{ z  e.  ~P dom  R  |  z  ~<_  om } )
223222biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  ->  A. w  e.  ran  g  w  e. 
{ z  e.  ~P dom  R  |  z  ~<_  om } )
224 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  w  ->  (
z  ~<_  om  <->  w  ~<_  om )
)
225224elrab 3184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  { z  e. 
~P dom  R  | 
z  ~<_  om }  <->  ( w  e.  ~P dom  R  /\  w  ~<_  om ) )
226225simprbi 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  { z  e. 
~P dom  R  | 
z  ~<_  om }  ->  w  ~<_  om )
227226ralimi 2796 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. w  e.  ran  g  w  e.  { z  e. 
~P dom  R  | 
z  ~<_  om }  ->  A. w  e.  ran  g  w  ~<_  om )
228223, 227syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  ->  A. w  e.  ran  g  w  ~<_  om )
229 unictb 9018 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  g  ~<_  om  /\  A. w  e.  ran  g  w  ~<_  om )  ->  U. ran  g  ~<_  om )
230221, 228, 229syl2an 485 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g  Fn  X  /\  X  ~<_  om )  /\  ran  g  C_  { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  U. ran  g  ~<_  om )
231217, 218, 210, 230syl21anc 1291 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  U. ran  g  ~<_  om )
232 ctex 7602 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. ran  g  ~<_  om  ->  U.
ran  g  e.  _V )
233 elpwg 3950 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. ran  g  e.  _V  ->  ( U. ran  g  e.  ~P dom  R  <->  U. ran  g  C_ 
dom  R ) )
234231, 232, 2333syl 18 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* 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 ) )
235215, 234mpbird 240 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  U. ran  g  e.  ~P dom  R )
236 simpl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  C_  U. (
g `  y )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) )  ->  A  C_ 
U. ( g `  y ) )
237236ralimi 2796 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  X  ( A  C_  U. ( g `
 y )  /\ Σ* w  e.  ( g `  y
) ( R `  w )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) )  ->  A. y  e.  X  A  C_  U. (
g `  y )
)
238 fvssunirn 5902 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g `
 y )  C_  U.
ran  g
239238unissi 4213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U. (
g `  y )  C_ 
U. U. ran  g
240 sstr 3426 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  C_  U. (
g `  y )  /\  U. ( g `  y )  C_  U. U. ran  g )  ->  A  C_ 
U. U. ran  g )
241239, 240mpan2 685 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A 
C_  U. ( g `  y )  ->  A  C_ 
U. U. ran  g )
242241ralimi 2796 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. y  e.  X  A  C_ 
U. ( g `  y )  ->  A. y  e.  X  A  C_  U. U. ran  g )
243 iunss 4310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U_ y  e.  X  A  C_ 
U. U. ran  g  <->  A. y  e.  X  A  C_  U. U. ran  g )
244242, 243sylibr 217 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  X  A  C_ 
U. ( g `  y )  ->  U_ y  e.  X  A  C_  U. U. ran  g )
245237, 244syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  X  ( A  C_  U. ( g `
 y )  /\ Σ* w  e.  ( g `  y
) ( R `  w )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) )  ->  U_ y  e.  X  A  C_  U. U. ran  g )
246245adantl 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  U_ y  e.  X  A  C_  U. U. ran  g )
247235, 246, 231jca32 544 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* 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 ) ) )
248 unieq 4198 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  U. ran  g  ->  U. z  =  U. U.
ran  g )
249248sseq2d 3446 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  U. ran  g  ->  ( U_ y  e.  X  A  C_  U. z  <->  U_ y  e.  X  A  C_ 
U. U. ran  g ) )
250 breq1 4398 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  U. ran  g  ->  ( z  ~<_  om  <->  U. ran  g  ~<_  om ) )
251249, 250anbi12d 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) )
252251elrab 3184 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
253247, 252sylibr 217 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* 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 ) } )
254 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  w  ->  ( R `  c )  =  ( R `  w ) )
255254cbvesumv 28938 . . . . . . . . . . . . . . . . . 18  |- Σ* c  e.  U. ran  g ( R `  c )  = Σ* w  e. 
U. ran  g ( R `  w )
256 esumeq1 28929 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  U. ran  g  -> Σ* w  e.  x ( R `
 w )  = Σ* w  e.  U. ran  g
( R `  w
) )
257256eqeq2d 2481 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  U. ran  g  ->  (Σ* c  e.  U. ran  g ( R `  c )  = Σ* w  e.  x ( R `  w )  <-> Σ* c  e.  U. ran  g ( R `  c )  = Σ* w  e. 
U. ran  g ( R `  w )
) )
258257rspcev 3136 . . . . . . . . . . . . . . . . . 18  |-  ( ( U. ran  g  e. 
{ z  e.  ~P dom  R  |  ( U_ y  e.  X  A  C_ 
U. z  /\  z  ~<_  om ) }  /\ Σ* c  e.  U. ran  g ( R `  c )  = Σ* 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 ) }Σ* c  e.  U. ran  g ( R `  c )  = Σ* w  e.  x ( R `  w ) )
259253, 255, 258sylancl 675 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* 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 ) }Σ*
c  e.  U. ran  g ( R `  c )  = Σ* w  e.  x ( R `  w ) )
260 esumex 28924 . . . . . . . . . . . . . . . . . 18  |- Σ* c  e.  U. ran  g ( R `  c )  e.  _V
261 eqid 2471 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  { z  e. 
~P dom  R  | 
( U_ y  e.  X  A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x ( R `  w ) )  =  ( x  e.  {
z  e.  ~P dom  R  |  ( U_ y  e.  X  A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ*
w  e.  x ( R `  w ) )
262261elrnmpt 5087 . . . . . . . . . . . . . . . . . 18  |-  (Σ* c  e. 
U. ran  g ( R `  c )  e.  _V  ->  (Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) )  <->  E. x  e.  { z  e.  ~P dom  R  |  ( U_ y  e.  X  A  C_ 
U. z  /\  z  ~<_  om ) }Σ* c  e.  U. ran  g ( R `  c )  = Σ* w  e.  x ( R `  w ) ) )
263260, 262ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  (Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) )  <->  E. x  e.  { z  e.  ~P dom  R  |  ( U_ y  e.  X  A  C_ 
U. z  /\  z  ~<_  om ) }Σ* c  e.  U. ran  g ( R `  c )  = Σ* w  e.  x ( R `  w ) )
264259, 263sylibr 217 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> Σ* 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 ) }  |-> Σ* w  e.  x ( R `  w ) ) )
265112a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  <  Or  ( 0 [,] +oo ) )
266 omscl 29192 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) }  |-> Σ* w  e.  x ( R `  w ) )  C_  ( 0 [,] +oo ) )
26726, 27, 175, 266syl3anc 1292 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( U_ y  e.  X  A  C_ 
U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  C_  (
0 [,] +oo )
)
268 xrge0infss 28415 . . . . . . . . . . . . . . . . . . 19  |-  ( ran  ( x  e.  {
z  e.  ~P dom  R  |  ( U_ y  e.  X  A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ*
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 ) }  |-> Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) u  < 
t ) ) )
269267, 268syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) }  |-> Σ* 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 ) }  |-> Σ* w  e.  x
( R `  w
) ) u  < 
t ) ) )
270265, 269inflb 8023 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  (Σ* 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 ) }  |-> Σ*
w  e.  x ( R `  w ) )  ->  -. Σ* 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 ) }  |-> Σ*
w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) ) )
27129fveq1i 5880 . . . . . . . . . . . . . . . . . . . 20  |-  ( M `
 U_ y  e.  X  A )  =  ( (toOMeas `  R ) `  U_ y  e.  X  A )
272169, 37sseqtrd 3454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U_ y  e.  X  A  C_  U. Q )
273 omsfval 29191 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) }  |-> Σ* w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) )
27426, 27, 272, 273syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) }  |-> Σ* w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) )
275271, 274syl5eq 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) }  |-> Σ* w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) )
276275breq2d 4407 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  (Σ* c  e.  U. ran  g ( R `  c )  <  ( M `  U_ y  e.  X  A )  <-> Σ* 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 ) }  |-> Σ*
w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) ) )
277276notbid 301 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -. Σ* c  e.  U. ran  g ( R `  c )  <  ( M `  U_ y  e.  X  A )  <->  -. Σ* 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 ) }  |-> Σ*
w  e.  x ( R `  w ) ) ,  ( 0 [,] +oo ) ,  <  ) ) )
278270, 277sylibrd 242 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  (Σ* 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 ) }  |-> Σ*
w  e.  x ( R `  w ) )  ->  -. Σ* c  e.  U. ran  g ( R `  c )  <  ( M `  U_ y  e.  X  A ) ) )
279166, 264, 278sylc 61 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  -. Σ* c  e.  U. ran  g
( R `  c
)  <  ( M `  U_ y  e.  X  A ) )
280 biid 244 . . . . . . . . . . . . . . 15  |-  ( -. Σ* c  e.  U. ran  g
( R `  c
)  <  ( M `  U_ y  e.  X  A )  <->  -. Σ* c  e.  U. ran  g ( R `  c )  <  ( M `  U_ y  e.  X  A ) )
281279, 280sylib 201 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  ->  -. Σ* c  e.  U. ran  g
( R `  c
)  <  ( M `  U_ y  e.  X  A ) )
282 xrlenlt 9717 . . . . . . . . . . . . . . 15  |-  ( ( ( M `  U_ y  e.  X  A )  e.  RR*  /\ Σ* c  e.  U. ran  g ( R `  c )  e.  RR* )  ->  ( ( M `
 U_ y  e.  X  A )  <_ Σ* c  e.  U. ran  g ( R `  c )  <->  -. Σ* c  e.  U. ran  g ( R `  c )  <  ( M `  U_ y  e.  X  A ) ) )
283178, 204, 282syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
( ( M `  U_ y  e.  X  A
)  <_ Σ* c  e.  U. ran  g ( R `  c )  <->  -. Σ* c  e.  U. ran  g ( R `  c )  <  ( M `  U_ y  e.  X  A ) ) )
284281, 283mpbird 240 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  -> 
( M `  U_ y  e.  X  A )  <_ Σ* c  e.  U. ran  g
( R `  c
) )
285 nfv 1769 . . . . . . . . . . . . . . . . . . 19  |-  F/ y  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }
28622, 285nfan 2031 . . . . . . . . . . . . . . . . . 18  |-  F/ y ( ( ( (
ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )
287 nfra1 2785 . . . . . . . . . . . . . . . . . 18  |-  F/ y A. y  e.  X  ( A  C_  U. (
g `  y )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) )
288286, 287nfan 2031 . . . . . . . . . . . . . . . . 17  |-  F/ y ( ( ( ( ( ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )
289 simp-6l 788 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  /\  y  e.  X )  ->  ph )
290 simpllr 777 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  /\  y  e.  X )  ->  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )
291 simpr 468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\ Σ* 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 )  /\ Σ* w  e.  ( g `  y ) ( R `
 w )  < 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) ) )  /\  y  e.  X )  ->  y  e.  X )
29227ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  R : Q --> ( 0 [,] +oo ) )
293 simpllr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 } )
294 simplr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  y  e.  X )
295293, 294ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 } )
296189, 295sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  (
g `  y )  e.  ~P dom  R )
297296elpwid 3952 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  (
g `  y )  C_ 
dom  R )
298292, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  dom  R  =  Q )
299297, 298sseqtrd 3454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  (
g `  y )  C_  Q )
300 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  w  e.  ( g `  y
) )
301299, 300sseldd 3419 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  w  e.  Q )
302292, 301ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  ( R `  w )  e.  ( 0 [,] +oo ) )
303302ralrimiva 2809 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  y  e.  X )  ->  A. w  e.  ( g `  y ) ( R `  w
)  e.  ( 0 [,] +oo ) )
304 fvex 5889 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g `
 y )  e. 
_V
305 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ w
( g `  y
)
306305esumcl 28925 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( g `  y
)