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

Theorem omssubadd 28961
Description: A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.)
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  c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omssubadd.b . . . . . 6  |-  ( ph  ->  X  ~<_  om )
2 nnenom 12190 . . . . . . 7  |-  NN  ~~  om
32ensymi 7626 . . . . . 6  |-  om  ~~  NN
4 domentr 7635 . . . . . 6  |-  ( ( X  ~<_  om  /\  om  ~~  NN )  ->  X  ~<_  NN )
51, 3, 4sylancl 666 . . . . 5  |-  ( ph  ->  X  ~<_  NN )
6 brdomi 7588 . . . . 5  |-  ( X  ~<_  NN  ->  E. f 
f : X -1-1-> NN )
75, 6syl 17 . . . 4  |-  ( ph  ->  E. f  f : X -1-1-> NN )
87adantr 466 . . 3  |-  ( (
ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  ->  E. f  f : X -1-1-> NN )
9 simplll 766 . . . . . . . . . 10  |-  ( ( ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  ->  ph )
10 ctex 28135 . . . . . . . . . . 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 1754 . . . . . . . . . . . . 13  |-  F/ y
ph
14 nfcv 2591 . . . . . . . . . . . . . . 15  |-  F/_ y X
1514nfesum1 28700 . . . . . . . . . . . . . 14  |-  F/_ yΣ* y  e.  X ( M `  A )
16 nfcv 2591 . . . . . . . . . . . . . 14  |-  F/_ y RR
1715, 16nfel 2604 . . . . . . . . . . . . 13  |-  F/ yΣ* y  e.  X ( M `
 A )  e.  RR
1813, 17nfan 1986 . . . . . . . . . . . 12  |-  F/ y ( ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )
19 nfv 1754 . . . . . . . . . . . 12  |-  F/ y  f : X -1-1-> NN
2018, 19nfan 1986 . . . . . . . . . . 11  |-  F/ y ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )
21 nfv 1754 . . . . . . . . . . 11  |-  F/ y  e  e.  RR+
2220, 21nfan 1986 . . . . . . . . . 10  |-  F/ y ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )
239adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  ph )
24 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  y  e.  X )
2511adantr 466 . . . . . . . . . . . . . . . . . . . 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 28957 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Q  e.  V  /\  R : Q --> ( 0 [,] +oo ) )  ->  (toOMeas `  R ) : ~P U. dom  R --> ( 0 [,] +oo ) )
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  M  =  (toOMeas `  R )
3029feq1i 5738 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M : ~P U. dom  R --> ( 0 [,] +oo ) 
<->  (toOMeas `  R ) : ~P U. dom  R --> ( 0 [,] +oo ) )
3128, 30sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Q  e.  V  /\  R : Q --> ( 0 [,] +oo ) )  ->  M : ~P U.
dom  R --> ( 0 [,] +oo ) )
3226, 27, 31syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  M : ~P U. dom  R --> ( 0 [,] +oo ) )
3332adantr 466 . . . . . . . . . . . . . . . . . . . . . 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 5750 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( R : Q --> ( 0 [,] +oo )  ->  dom  R  =  Q )
3627, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  dom  R  =  Q )
3736unieqd 4232 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  U. dom  R  = 
U. Q )
3837adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  X )  ->  U. dom  R  =  U. Q )
3934, 38sseqtr4d 3507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  X )  ->  A  C_ 
U. dom  R )
40 uniexg 6602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Q  e.  V  ->  U. Q  e.  _V )
4126, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  U. Q  e.  _V )
4241adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  X )  ->  U. Q  e.  _V )
43 ssexg 4571 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  C_  U. Q  /\  U. Q  e.  _V )  ->  A  e.  _V )
4434, 42, 43syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  X )  ->  A  e.  _V )
45 elpwg 3993 . . . . . . . . . . . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  /\  y  e.  X
)  ->  ( M `  A )  e.  ( 0 [,] +oo )
)
50 simpr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  -> Σ* y  e.  X ( M `  A )  e.  RR )
5118, 25, 49, 50esumcvgre 28751 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\ Σ* y  e.  X
( M `  A
)  e.  RR )  /\  y  e.  X
)  ->  ( M `  A )  e.  RR )
5251adantlr 719 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  ( M `  A )  e.  RR )
5352adantlr 719 . . . . . . . . . . . . . . . . 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 11312 . . . . . . . . . . . . . . . . . . 19  |-  RR+  C_  RR
55 simplr 760 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  e  e.  RR+ )
56 2rp 11307 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  RR+
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  2  e.  RR+ )
58 df-f1 5606 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : X -1-1-> NN  <->  ( f : X --> NN  /\  Fun  `' f ) )
5958simplbi 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f : X -1-1-> NN  ->  f : X --> NN )
6059adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 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 11039 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
f `  y )  e.  ZZ )
6357, 62rpexpcld 12436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
2 ^ ( f `
 y ) )  e.  RR+ )
6463adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( 2 ^ ( f `  y ) )  e.  RR+ )
6555, 64rpdivcld 11358 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( e  /  ( 2 ^ ( f `  y
) ) )  e.  RR+ )
6654, 65sseldi 3468 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( e  /  ( 2 ^ ( f `  y
) ) )  e.  RR )
6766adantl3r 754 . . . . . . . . . . . . . . . . 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 11525 . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . 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 28188 . . . . . . . . . . . . . . . . . . . 20  |-  RR+  =  ( 0 (,) +oo )
72 ioossicc 11720 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) +oo )  C_  ( 0 [,] +oo )
7371, 72eqsstri 3500 . . . . . . . . . . . . . . . . . . 19  |-  RR+  C_  (
0 [,] +oo )
7473, 65sseldi 3468 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( e  /  ( 2 ^ ( f `  y
) ) )  e.  ( 0 [,] +oo ) )
7574adantl3r 754 . . . . . . . . . . . . . . . . 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 28183 . . . . . . . . . . . . . . . 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 2518 . . . . . . . . . . . . . . 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 3468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  e  e.  RR )
7978adantl3r 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  e  e.  RR )
8054, 63sseldi 3468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
2 ^ ( f `
 y ) )  e.  RR )
8180adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X
)  ->  ( 2 ^ ( f `  y ) )  e.  RR )
8281adantl3r 754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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 760 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  e  e.  RR+ )
8483rpgt0d 11344 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  0  <  e )
85 2re 10679 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
8685a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  2  e.  RR )
8762adantllr 723 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\ Σ* y  e.  X ( M `  A )  e.  RR )  /\  f : X -1-1-> NN )  /\  y  e.  X )  ->  (
f `  y )  e.  ZZ )
8887adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 10701 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <  2
9089a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  0  <  2 )
91 expgt0 12302 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2  e.  RR  /\  ( f `  y
)  e.  ZZ  /\  0  <  2 )  -> 
0  <  ( 2 ^ ( f `  y ) ) )
9286, 88, 90, 91syl3anc 1264 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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 10542 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 10196 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 213 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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 ) ) ) ) )
96 ovex 6333 . . . . . . . . . . . . . . . . . 18  |-  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) )  e. 
_V
97 fvex 5891 . . . . . . . . . . . . . . . . . 18  |-  ( M `
 A )  e. 
_V
9896, 97brcnv 5037 . . . . . . . . . . . . . . . . 17  |-  ( ( ( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  ( M `  A )  <->  ( M `  A )  <  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) )
9995, 98sylibr 215 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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
) ) ) ) `'  <  ( M `  A ) )
10029fveq1i 5882 . . . . . . . . . . . . . . . . . 18  |-  ( M `
 A )  =  ( (toOMeas `  R
) `  A )
10126adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  X )  ->  Q  e.  V )
10227adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  X )  ->  R : Q --> ( 0 [,] +oo ) )
103 omsfval 28955 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Q  e.  V  /\  R : Q --> ( 0 [,] +oo )  /\  A  C_  U. Q )  ->  ( (toOMeas `  R
) `  A )  =  sup ( ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )
104101, 102, 34, 103syl3anc 1264 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  X )  ->  (
(toOMeas `  R ) `  A )  =  sup ( ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )
105100, 104syl5eq 2482 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  X )  ->  ( M `  A )  =  sup ( ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )
1069, 105sylan 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ Σ* y  e.  X ( M `
 A )  e.  RR )  /\  f : X -1-1-> NN )  /\  e  e.  RR+ )  /\  y  e.  X )  ->  ( M `  A )  =  sup ( ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )
10799, 106breqtrd 4450 . . . . . . . . . . . . . . 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
) ) ) ) `'  <  sup ( ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )
10877, 107jca 534 . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  <  sup ( ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) ) )
109 iccssxr 11717 . . . . . . . . . . . . . . . . . . 19  |-  ( 0 [,] +oo )  C_  RR*
110 xrltso 11440 . . . . . . . . . . . . . . . . . . 19  |-  <  Or  RR*
111 soss 4793 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0 [,] +oo )  C_ 
RR*  ->  (  <  Or  RR* 
->  <  Or  ( 0 [,] +oo ) ) )
112109, 110, 111mp2 9 . . . . . . . . . . . . . . . . . 18  |-  <  Or  ( 0 [,] +oo )
113 cnvso 5395 . . . . . . . . . . . . . . . . . 18  |-  (  < 
Or  ( 0 [,] +oo )  <->  `'  <  Or  (
0 [,] +oo )
)
114112, 113mpbi 211 . . . . . . . . . . . . . . . . 17  |-  `'  <  Or  ( 0 [,] +oo )
115114a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  X )  ->  `'  <  Or  ( 0 [,] +oo ) )
116 omscl 28956 . . . . . . . . . . . . . . . . . 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 ) )
117101, 102, 47, 116syl3anc 1264 . . . . . . . . . . . . . . . . 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 )
)
118 xrge0infss 28181 . . . . . . . . . . . . . . . . 17  |-  ( ran  ( x  e.  {
z  e.  ~P dom  R  |  ( 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  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  -.  e `'  <  t  /\  A. t  e.  ( 0 [,] +oo ) ( t `'  <  e  ->  E. u  e.  ran  ( x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) t `'  <  u ) ) )
119117, 118syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  X )  ->  E. e  e.  ( 0 [,] +oo ) ( A. t  e.  ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  -.  e `'  <  t  /\  A. t  e.  ( 0 [,] +oo ) ( t `'  <  e  ->  E. u  e.  ran  ( x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) t `'  <  u ) ) )
120115, 119suplub 7980 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  X )  ->  (
( ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) )  e.  ( 0 [,] +oo )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  <  sup ( ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) )  ->  E. u  e.  ran  ( x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u ) )
121120imp 430 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  X )  /\  (
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) )  e.  ( 0 [,] +oo )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  <  sup ( ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ,  ( 0 [,] +oo ) ,  `'  <  ) ) )  ->  E. u  e.  ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u )
12223, 24, 108, 121syl21anc 1263 . . . . . . . . . . . . 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
) ) ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u )
123 eqid 2429 . . . . . . . . . . . . . . . . . . 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 ) )
124 esumex 28689 . . . . . . . . . . . . . . . . . . 19  |- Σ* w  e.  x
( R `  w
)  e.  _V
125123, 124elrnmpti 5105 . . . . . . . . . . . . . . . . . 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 ) )
126125anbi1i 699 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  u )  <->  ( E. x  e.  { z  e.  ~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) } u  = Σ* w  e.  x
( R `  w
)  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u ) )
127 r19.41v 2987 . . . . . . . . . . . . . . . . 17  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  ( u  = Σ* w  e.  x ( R `  w )  /\  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) `'  <  u )  <->  ( E. x  e.  { z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) } u  = Σ* w  e.  x ( R `
 w )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  <  u
) )
128126, 127bitr4i 255 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  u )  <->  E. x  e.  { z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  ( u  = Σ* w  e.  x ( R `  w )  /\  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) `'  <  u ) )
129128exbii 1714 . . . . . . . . . . . . . . 15  |-  ( E. u ( u  e. 
ran  ( x  e. 
{ z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  u )  <->  E. u E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  ( u  = Σ* w  e.  x ( R `  w )  /\  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) `'  <  u ) )
130 df-rex 2788 . . . . . . . . . . . . . . 15  |-  ( E. u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u  <->  E. u
( u  e.  ran  ( x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  u ) )
131 rexcom4 3107 . . . . . . . . . . . . . . 15  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) } E. u
( u  = Σ* w  e.  x ( R `  w )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  u )  <->  E. u E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  ( u  = Σ* w  e.  x ( R `  w )  /\  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) `'  <  u ) )
132129, 130, 1313bitr4i 280 . . . . . . . . . . . . . 14  |-  ( E. u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u  <->  E. x  e.  { z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) } E. u
( u  = Σ* w  e.  x ( R `  w )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  u ) )
133 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( u  = Σ* w  e.  x
( R `  w
)  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u )  -> 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  <  u
)
134 simpl 458 . . . . . . . . . . . . . . . . 17  |-  ( ( u  = Σ* w  e.  x
( R `  w
)  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u )  ->  u  = Σ* w  e.  x
( R `  w
) )
135133, 134breqtrd 4450 . . . . . . . . . . . . . . . 16  |-  ( ( u  = Σ* w  e.  x
( R `  w
)  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u )  -> 
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  x
( R `  w
) )
136135exlimiv 1769 . . . . . . . . . . . . . . 15  |-  ( E. u ( u  = Σ* w  e.  x ( R `
 w )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  <  u
)  ->  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) )
137136reximi 2900 . . . . . . . . . . . . . 14  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) } E. u
( u  = Σ* w  e.  x ( R `  w )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  <  u )  ->  E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) )
138132, 137sylbi 198 . . . . . . . . . . . . 13  |-  ( E. u  e.  ran  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  |-> Σ* w  e.  x
( R `  w
) ) ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  <  u  ->  E. x  e.  { z  e.  ~P dom  R  |  ( A 
C_  U. z  /\  z  ~<_  om ) }  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) )
139122, 138syl 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 ) }  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) )
140 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( A  C_  U. z  /\  z  ~<_  om )  ->  z  ~<_  om )
141140a1i 11 . . . . . . . . . . . . . . 15  |-  ( z  e.  ~P dom  R  ->  ( ( A  C_  U. z  /\  z  ~<_  om )  ->  z  ~<_  om )
)
142141ss2rabi 3549 . . . . . . . . . . . . . 14  |-  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  C_  { z  e.  ~P dom  R  |  z  ~<_  om }
143 rexss 3534 . . . . . . . . . . . . . 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 ) }  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w )  <->  E. x  e.  { z  e.  ~P dom  R  |  z  ~<_  om }  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  x ( R `  w ) ) ) )
144142, 143ax-mp 5 . . . . . . . . . . . . 13  |-  ( E. x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w )  <->  E. x  e.  { z  e.  ~P dom  R  |  z  ~<_  om }  (
x  e.  { z  e.  ~P dom  R  |  ( A  C_  U. z  /\  z  ~<_  om ) }  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  x ( R `  w ) ) )
145 unieq 4230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  x  ->  U. z  =  U. x )
146145sseq2d 3498 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  x  ->  ( A  C_  U. z  <->  A  C_  U. x
) )
147 breq1 4429 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  x  ->  (
z  ~<_  om  <->  x  ~<_  om )
)
148146, 147anbi12d 715 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  x  ->  (
( A  C_  U. z  /\  z  ~<_  om )  <->  ( A  C_  U. x  /\  x  ~<_  om )
) )
149148elrab 3235 . . . . . . . . . . . . . . . . . 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 ) ) )
150149simprbi 465 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  ->  ( A  C_  U. x  /\  x  ~<_  om ) )
151150simpld 460 . . . . . . . . . . . . . . . 16  |-  ( x  e.  { z  e. 
~P dom  R  | 
( A  C_  U. z  /\  z  ~<_  om ) }  ->  A  C_  U. x
)
152151a1i 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 ) )
153152anim1d 566 . . . . . . . . . . . . . 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 ) }  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  x ( R `  w ) )  ->  ( A  C_ 
U. x  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  x ( R `  w ) ) ) )
154153reximdv 2906 . . . . . . . . . . . . 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 ) }  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  x ( R `  w ) )  ->  E. x  e.  { z  e.  ~P dom  R  |  z  ~<_  om }  ( A  C_  U. x  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) ) ) )
155144, 154syl5bi 220 . . . . . . . . . . . 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 ) }  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w )  ->  E. x  e.  {
z  e.  ~P dom  R  |  z  ~<_  om } 
( A  C_  U. x  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  x
( R `  w
) ) ) )
156139, 155mpd 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  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) ) )
157156ex 435 . . . . . . . . . 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  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) ) ) )
15822, 157ralrimi 2832 . . . . . . . . 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  /\  ( ( M `  A )  +  ( e  / 
( 2 ^ (
f `  y )
) ) ) `'  < Σ* w  e.  x ( R `  w ) ) )
159 unieq 4230 . . . . . . . . . . . . 13  |-  ( x  =  ( g `  y )  ->  U. x  =  U. ( g `  y ) )
160159sseq2d 3498 . . . . . . . . . . . 12  |-  ( x  =  ( g `  y )  ->  ( A  C_  U. x  <->  A  C_  U. (
g `  y )
) )
161 esumeq1 28694 . . . . . . . . . . . . 13  |-  ( x  =  ( g `  y )  -> Σ* w  e.  x
( R `  w
)  = Σ* w  e.  (
g `  y )
( R `  w
) )
162161breq2d 4438 . . . . . . . . . . . 12  |-  ( x  =  ( g `  y )  ->  (
( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  x
( R `  w
)  <->  ( ( M `
 A )  +  ( e  /  (
2 ^ ( f `
 y ) ) ) ) `'  < Σ* w  e.  ( g `  y
) ( R `  w ) ) )
163160, 162anbi12d 715 . . . . . . . . . . 11  |-  ( x  =  ( g `  y )  ->  (
( A  C_  U. x  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  x
( R `  w
) )  <->  ( A  C_ 
U. ( g `  y )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  ( g `
 y ) ( R `  w ) ) ) )
164163ac6sg 8916 . . . . . . . . . 10  |-  ( X  e.  _V  ->  ( A. y  e.  X  E. x  e.  { z  e.  ~P dom  R  |  z  ~<_  om }  ( A  C_  U. x  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  x
( R `  w
) )  ->  E. g
( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  /\  A. y  e.  X  ( A  C_ 
U. ( g `  y )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  ( g `
 y ) ( R `  w ) ) ) ) )
165164imp 430 . . . . . . . . 9  |-  ( ( X  e.  _V  /\  A. y  e.  X  E. x  e.  { z  e.  ~P dom  R  | 
z  ~<_  om }  ( A 
C_  U. x  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  x ( R `  w ) ) )  ->  E. g
( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  /\  A. y  e.  X  ( A  C_ 
U. ( g `  y )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  ( g `
 y ) ( R `  w ) ) ) )
16612, 158, 165syl2anc 665 . . . . . . . 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 )  /\  (
( M `  A
)  +  ( e  /  ( 2 ^ ( f `  y
) ) ) ) `'  < Σ* w  e.  ( g `
 y ) ( R `  w ) ) ) )
1679ad2antrr 730 . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  ph )
16839ralrimiva 2846 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. y  e.  X  A  C_  U. dom  R
)
169 iunss 4343 . . . . . . . . . . . . . . . . . 18  |-  ( U_ y  e.  X  A  C_ 
U. dom  R  <->  A. y  e.  X  A  C_  U. dom  R )
170168, 169sylibr 215 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  U_ y  e.  X  A  C_  U. dom  R
)
17144ralrimiva 2846 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. y  e.  X  A  e.  _V )
172 iunexg 6783 . . . . . . . . . . . . . . . . . . 19  |-  ( ( X  e.  _V  /\  A. y  e.  X  A  e.  _V )  ->  U_ y  e.  X  A  e.  _V )
17311, 171, 172syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U_ y  e.  X  A  e.  _V )
174 elpwg 3993 . . . . . . . . . . . . . . . . . 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 )
)
175173, 174syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U_ y  e.  X  A  e.  ~P U.
dom  R  <->  U_ y  e.  X  A  C_  U. dom  R
) )
176170, 175mpbird 235 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  U_ y  e.  X  A  e.  ~P U. dom  R )
17732, 176ffvelrnd 6038 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( M `  U_ y  e.  X  A )  e.  ( 0 [,] +oo ) )
178109, 177sseldi 3468 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M `  U_ y  e.  X  A )  e.  RR* )
179167, 178syl 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
( M `  U_ y  e.  X  A )  e.  RR* )
180 simplr 760 . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )
18125ad4antr 736 . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  X  e.  _V )
182 fex 6153 . . . . . . . . . . . . . . . . 17  |-  ( ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  /\  X  e.  _V )  ->  g  e.  _V )
183180, 181, 182syl2anc 665 . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
g  e.  _V )
184 rnexg 6739 . . . . . . . . . . . . . . . 16  |-  ( g  e.  _V  ->  ran  g  e.  _V )
185 uniexg 6602 . . . . . . . . . . . . . . . 16  |-  ( ran  g  e.  _V  ->  U.
ran  g  e.  _V )
186183, 184, 1853syl 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  U. ran  g  e.  _V )
187 simp-5l 776 . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  ph )
18827ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  c  e.  U. ran  g
)  ->  R : Q
--> ( 0 [,] +oo ) )
189 frn 5752 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om } )
190 ssrab2 3552 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { z  e.  ~P dom  R  |  z  ~<_  om }  C_  ~P dom  R
191189, 190syl6ss 3482 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  ran  g  C_  ~P dom  R )
192191unissd 4246 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  U.
ran  g  C_  U. ~P dom  R )
193 unipw 4672 . . . . . . . . . . . . . . . . . . . . . 22  |-  U. ~P dom  R  =  dom  R
194192, 193syl6sseq 3516 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  U.
ran  g  C_  dom  R )
195194adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  U. ran  g  C_  dom  R )
19636adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  dom  R  =  Q )
197195, 196sseqtrd 3506 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  U. ran  g  C_  Q )
198197sselda 3470 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  c  e.  U. ran  g
)  ->  c  e.  Q )
199188, 198ffvelrnd 6038 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  c  e.  U. ran  g
)  ->  ( R `  c )  e.  ( 0 [,] +oo )
)
200199ralrimiva 2846 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  g : X
--> { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  A. c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo ) )
201187, 180, 200syl2anc 665 . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  A. c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo )
)
202 nfcv 2591 . . . . . . . . . . . . . . . 16  |-  F/_ c U. ran  g
203202esumcl 28690 . . . . . . . . . . . . . . 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 )
)
204186, 201, 203syl2anc 665 . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> Σ* c  e.  U. ran  g ( R `  c )  e.  ( 0 [,] +oo ) )
205109, 204sseldi 3468 . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> Σ* c  e.  U. ran  g ( R `  c )  e.  RR* )
206 simp-5r 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> Σ* y  e.  X ( M `  A )  e.  RR )
207206rexrd 9689 . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> Σ* y  e.  X ( M `  A )  e.  RR* )
208 simpllr 767 . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
e  e.  RR+ )
209208rpxrd 11342 . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
e  e.  RR* )
210207, 209xaddcld 11587 . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
(Σ* y  e.  X ( M `  A ) +e e )  e.  RR* )
211189ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  ran  g  C_  { z  e.  ~P dom  R  |  z  ~<_  om } )
212 sstr 3478 . . . . . . . . . . . . . . . . . . . . . . . 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 )
213190, 212mpan2 675 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  ->  ran  g  C_  ~P dom  R
)
214 sspwuni 4391 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ran  g  C_  ~P dom  R  <->  U. ran  g  C_  dom  R )
215213, 214sylib 199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  ->  U. ran  g  C_  dom  R )
216211, 215syl 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  U. ran  g  C_  dom  R )
217 ffn 5746 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }  ->  g  Fn  X )
218217ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
g  Fn  X )
219167, 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  X  ~<_  om )
220 fnct 28140 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g  Fn  X  /\  X  ~<_  om )  ->  g  ~<_  om )
221 rnct 28143 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g  ~<_  om  ->  ran  g  ~<_  om )
222220, 221syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g  Fn  X  /\  X  ~<_  om )  ->  ran  g  ~<_  om )
223 dfss3 3460 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
224223biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
225 breq1 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  w  ->  (
z  ~<_  om  <->  w  ~<_  om )
)
226225elrab 3235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  e.  { z  e. 
~P dom  R  | 
z  ~<_  om }  <->  ( w  e.  ~P dom  R  /\  w  ~<_  om ) )
227226simprbi 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  { z  e. 
~P dom  R  | 
z  ~<_  om }  ->  w  ~<_  om )
228227ralimi 2825 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. w  e.  ran  g  w  e.  { z  e. 
~P dom  R  | 
z  ~<_  om }  ->  A. w  e.  ran  g  w  ~<_  om )
229224, 228syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  C_  { z  e.  ~P dom  R  | 
z  ~<_  om }  ->  A. w  e.  ran  g  w  ~<_  om )
230 unictb 8998 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  g  ~<_  om  /\  A. w  e.  ran  g  w  ~<_  om )  ->  U. ran  g  ~<_  om )
231222, 229, 230syl2an 479 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( g  Fn  X  /\  X  ~<_  om )  /\  ran  g  C_  { z  e.  ~P dom  R  |  z  ~<_  om } )  ->  U. ran  g  ~<_  om )
232218, 219, 211, 231syl21anc 1263 . . . . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  U. ran  g  ~<_  om )
233 ctex 28135 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. ran  g  ~<_  om  ->  U.
ran  g  e.  _V )
234 elpwg 3993 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. ran  g  e.  _V  ->  ( U. ran  g  e.  ~P dom  R  <->  U. ran  g  C_ 
dom  R ) )
235232, 233, 2343syl 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
( U. ran  g  e.  ~P dom  R  <->  U. ran  g  C_ 
dom  R ) )
236216, 235mpbird 235 . . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  U. ran  g  e.  ~P dom  R )
237 simpl 458 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  C_  U. (
g `  y )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) )  ->  A  C_ 
U. ( g `  y ) )
238237ralimi 2825 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  X  ( A  C_  U. ( g `
 y )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) )  ->  A. y  e.  X  A  C_  U. (
g `  y )
)
239 fvssunirn 5904 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g `
 y )  C_  U.
ran  g
240239unissi 4245 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U. (
g `  y )  C_ 
U. U. ran  g
241 sstr 3478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  C_  U. (
g `  y )  /\  U. ( g `  y )  C_  U. U. ran  g )  ->  A  C_ 
U. U. ran  g )
242240, 241mpan2 675 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A 
C_  U. ( g `  y )  ->  A  C_ 
U. U. ran  g )
243242ralimi 2825 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. y  e.  X  A  C_ 
U. ( g `  y )  ->  A. y  e.  X  A  C_  U. U. ran  g )
244 iunss 4343 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U_ y  e.  X  A  C_ 
U. U. ran  g  <->  A. y  e.  X  A  C_  U. U. ran  g )
245243, 244sylibr 215 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  X  A  C_ 
U. ( g `  y )  ->  U_ y  e.  X  A  C_  U. U. ran  g )
246238, 245syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  X  ( A  C_  U. ( g `
 y )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) )  ->  U_ y  e.  X  A  C_  U. U. ran  g )
247246adantl 467 . . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  U_ y  e.  X  A  C_  U. U. ran  g )
248236, 247, 232jca32 537 . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
( U. ran  g  e.  ~P dom  R  /\  ( U_ y  e.  X  A  C_  U. U. ran  g  /\  U. ran  g  ~<_  om ) ) )
249 unieq 4230 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  U. ran  g  ->  U. z  =  U. U.
ran  g )
250249sseq2d 3498 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  U. ran  g  ->  ( U_ y  e.  X  A  C_  U. z  <->  U_ y  e.  X  A  C_ 
U. U. ran  g ) )
251 breq1 4429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  U. ran  g  ->  ( z  ~<_  om  <->  U. ran  g  ~<_  om ) )
252250, 251anbi12d 715 . . . . . . . . . . . . . . . . . . . 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 ) ) )
253252elrab 3235 . . . . . . . . . . . . . . . . . . 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 ) ) )
254248, 253sylibr 215 . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  U. ran  g  e.  {
z  e.  ~P dom  R  |  ( U_ y  e.  X  A  C_  U. z  /\  z  ~<_  om ) } )
255 fveq2 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  w  ->  ( R `  c )  =  ( R `  w ) )
256255cbvesumv 28703 . . . . . . . . . . . . . . . . . 18  |- Σ* c  e.  U. ran  g ( R `  c )  = Σ* w  e. 
U. ran  g ( R `  w )
257 esumeq1 28694 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  U. ran  g  -> Σ* w  e.  x ( R `
 w )  = Σ* w  e.  U. ran  g
( R `  w
) )
258257eqeq2d 2443 . . . . . . . . . . . . . . . . . . 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 )
) )
259258rspcev 3188 . . . . . . . . . . . . . . . . . 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 ) )
260254, 256, 259sylancl 666 . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( 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 ) )
261 esumex 28689 . . . . . . . . . . . . . . . . . 18  |- Σ* c  e.  U. ran  g ( R `  c )  e.  _V
262 eqid 2429 . . . . . . . . . . . . . . . . . . 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 ) )
263262elrnmpt 5101 . . . . . . . . . . . . . . . . . 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 ) ) )
264261, 263ax-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 ) )
265260, 264sylibr 215 . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> Σ* 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 ) ) )
266114a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  `'  <  Or  ( 0 [,] +oo ) )
267 omscl 28956 . . . . . . . . . . . . . . . . . . . 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 ) )
26826, 27, 176, 267syl3anc 1264 . . . . . . . . . . . . . . . . . . 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 )
)
269 xrge0infss 28181 . . . . . . . . . . . . . . . . . . 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
) )  -.  e `'  <  t  /\  A. t  e.  ( 0 [,] +oo ) ( t `'  <  e  ->  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 ) ) t `'  <  u ) ) )
270268, 269syl 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
) )  -.  e `'  <  t  /\  A. t  e.  ( 0 [,] +oo ) ( t `'  <  e  ->  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 ) ) t `'  <  u ) ) )
271266, 270supub 7979 . . . . . . . . . . . . . . . . 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 ) )  ->  -.  sup ( 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 ) ,  `'  <  ) `'  < Σ* c  e. 
U. ran  g ( R `  c )
) )
27229fveq1i 5882 . . . . . . . . . . . . . . . . . . . 20  |-  ( M `
 U_ y  e.  X  A )  =  ( (toOMeas `  R ) `  U_ y  e.  X  A )
273170, 37sseqtrd 3506 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U_ y  e.  X  A  C_  U. Q )
274 omsfval 28955 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Q  e.  V  /\  R : Q --> ( 0 [,] +oo )  /\  U_ y  e.  X  A  C_ 
U. Q )  -> 
( (toOMeas `  R
) `  U_ y  e.  X  A )  =  sup ( 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 ) ,  `'  <  ) )
27526, 27, 273, 274syl3anc 1264 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( (toOMeas `  R
) `  U_ y  e.  X  A )  =  sup ( 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 ) ,  `'  <  ) )
276272, 275syl5eq 2482 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M `  U_ y  e.  X  A )  =  sup ( 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 ) ,  `'  <  ) )
277276breq1d 4436 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( M `  U_ y  e.  X  A
) `'  < Σ* c  e.  U. ran  g ( R `  c )  <->  sup ( 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 ) ,  `'  <  ) `'  < Σ* c  e. 
U. ran  g ( R `  c )
) )
278277notbid 295 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -.  ( M `
 U_ y  e.  X  A ) `'  < Σ* c  e. 
U. ran  g ( R `  c )  <->  -. 
sup ( 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 ) ,  `'  <  ) `'  < Σ* c  e. 
U. ran  g ( R `  c )
) )
279271, 278sylibrd 237 . . . . . . . . . . . . . . . 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 ) )  ->  -.  ( M `  U_ y  e.  X  A ) `'  < Σ* c  e.  U. ran  g ( R `  c ) ) )
280167, 265, 279sylc 62 . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  -.  ( M `  U_ y  e.  X  A ) `'  < Σ* c  e.  U. ran  g ( R `  c ) )
281 fvex 5891 . . . . . . . . . . . . . . . . 17  |-  ( M `
 U_ y  e.  X  A )  e.  _V
282281, 261brcnv 5037 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) )
283282notbii 297 . . . . . . . . . . . . . . 15  |-  ( -.  ( 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 ) )
284280, 283sylib 199 . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  ->  -. Σ* c  e.  U. ran  g
( R `  c
)  <  ( M `  U_ y  e.  X  A ) )
285 xrlenlt 9698 . . . . . . . . . . . . . . 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 ) ) )
286179, 205, 285syl2anc 665 . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
( ( 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 ) ) )
287284, 286mpbird 235 . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  -> 
( M `  U_ y  e.  X  A )  <_ Σ* c  e.  U. ran  g
( R `  c
) )
288 nfv 1754 . . . . . . . . . . . . . . . . . . 19  |-  F/ y  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om }
28922, 288nfan 1986 . . . . . . . . . . . . . . . . . 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 } )
290 nfra1 2813 . . . . . . . . . . . . . . . . . 18  |-  F/ y A. y  e.  X  ( A  C_  U. (
g `  y )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) )
291289, 290nfan 1986 . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )
292 simp-6l 778 . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  /\  y  e.  X )  ->  ph )
293 simpllr 767 . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  /\  y  e.  X )  ->  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )
294 simpr 462 . . . . . . . . . . . . . . . . . . 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 )  /\  ( ( M `  A )  +  ( e  /  ( 2 ^ ( f `  y ) ) ) ) `'  < Σ* w  e.  (
g `  y )
( R `  w
) ) )  /\  y  e.  X )  ->  y  e.  X )
29527ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  R : Q --> ( 0 [,] +oo ) )
296 simpllr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
297 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  y  e.  X )
298296, 297ffvelrnd 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 } )
299190, 298sseldi 3468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  (
g `  y )  e.  ~P dom  R )
300299elpwid 3995 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  (
g `  y )  C_ 
dom  R )
301295, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  dom  R  =  Q )
302300, 301sseqtrd 3506 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  (
g `  y )  C_  Q )
303 simpr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  w  e.  ( g `  y
) )
304302, 303sseldd 3471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  w  e.  Q )
305295, 304ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  g : X --> { z  e.  ~P dom  R  |  z  ~<_  om } )  /\  y  e.  X
)  /\  w  e.  ( g `  y
) )  ->  ( R `  w )  e.  ( 0 [,] +oo ) )
306305ralrimiva 2846 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  g : X --> { z  e. 
~P dom  R  | 
z  ~<_  om } )  /\  y  e.  X )  ->  A. w  e.  ( g `  y )