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 29128
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 12193 . . . . . . 7 |- NN ~~ om
32ensymi 7619 . . . . . 6 |- om ~~ NN
4 domentr 7628 . . . . . 6 |- ( ( X ~<_ om /\ om ~~ NN ) -> X ~<_ NN )
51, 3, 4sylancl 668 . . . . 5 |- ( ph -> X ~<_ NN )
6 brdomi 7580 . . . . 5 |- ( X ~<_ NN -> E. f f : X -1-1-> NN )
75, 6syl 17 . . . 4 |- ( ph -> E. f f : X -1-1-> NN )
87adantr 467 . . 3 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> E. f f : X -1-1-> NN )
9 simplll 768 . . . . . . . . . 10 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ph )
10 ctex 7584 . . . . . . . . . . 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 1761 . . . . . . . . . . . . 13 |- F/ y ph
14 nfcv 2592 . . . . . . . . . . . . . . 15 |- F/_ y X
1514nfesum1 28861 . . . . . . . . . . . . . 14 |- F/_ yΣ* y e. X ( M ` A )
16 nfcv 2592 . . . . . . . . . . . . . 14 |- F/_ y RR
1715, 16nfel 2604 . . . . . . . . . . . . 13 |- F/ yΣ* y e. X ( M ` A ) e. RR
1813, 17nfan 2011 . . . . . . . . . . . 12 |- F/ y ( ph /\ Σ* y e. X ( M ` A ) e. RR )
19 nfv 1761 . . . . . . . . . . . 12 |- F/ y f : X -1-1-> NN
2018, 19nfan 2011 . . . . . . . . . . 11 |- F/ y ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN )
21 nfv 1761 . . . . . . . . . . 11 |- F/ y e e. RR+
2220, 21nfan 2011 . . . . . . . . . 10 |- F/ y ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ )
239adantr 467 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ph )
24 simpr 463 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> y e. X )
2511adantr 467 . . . . . . . . . . . . . . . . . . . 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 29120 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- M = (toOMeas ` R )
3029feq1i 5720 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M : ~P U. dom R --> ( 0 [,] +oo ) <-> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
3128, 30sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
3226, 27, 31syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M : ~P U. dom R --> ( 0 [,] +oo ) )
3332adantr 467 . . . . . . . . . . . . . . . . . . . . . 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 5733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
3627, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> dom R = Q )
3736unieqd 4208 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> U. dom R = U. Q )
3837adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> U. dom R = U. Q )
3934, 38sseqtr4d 3469 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. X ) -> A C_ U. dom R )
40 uniexg 6588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( Q e. V -> U. Q e. _V )
4126, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> U. Q e. _V )
4241adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. X ) -> U. Q e. _V )
43 ssexg 4549 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
4434, 42, 43syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> A e. _V )
45 elpwg 3959 . . . . . . . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. X ) -> A e. ~P U. dom R )
4833, 47ffvelrnd 6023 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
4948adantlr 721 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
50 simpr 463 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> Σ* y e. X ( M ` A ) e. RR )
5118, 25, 49, 50esumcvgre 28912 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. RR )
5251adantlr 721 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( M ` A ) e. RR )
5352adantlr 721 . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . . 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 5587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : X -1-1-> NN <-> ( f : X --> NN /\ Fun `' f ) )
5958simplbi 462 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : X -1-1-> NN -> f : X --> NN )
6059adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> f : X --> NN )
6160ffvelrnda 6022 . . . . . . . . . . . . . . . . . . . . . . 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 12439 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
6463adantlr 721 . . . . . . . . . . . . . . . . . . . 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 3430 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
6766adantl3r 756 . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . . 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 28352 . . . . . . . . . . . . . . . . . . . 20 |- RR+ = ( 0 (,) +oo )
72 ioossicc 11720 . . . . . . . . . . . . . . . . . . . 20 |- ( 0 (,) +oo ) C_ ( 0 [,] +oo )
7371, 72eqsstri 3462 . . . . . . . . . . . . . . . . . . 19 |- RR+ C_ ( 0 [,] +oo )
7473, 65sseldi 3430 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
7574adantl3r 756 . . . . . . . . . . . . . . . . 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 28344 . . . . . . . . . . . . . . . 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 2530 . . . . . . . . . . . . . . 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 3430 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
7978adantl3r 756 . . . . . . . . . . . . . . . . . 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 3430 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
8180adantlr 721 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
8281adantl3r 756 . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
8483rpgt0d 11344 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < e )
85 2re 10679 . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
8887adantlr 721 . . . . . . . . . . . . . . . . . . 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 10701 . . . . . . . . . . . . . . . . . . . 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 12305 . . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. RR /\ ( f ` y ) e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ ( f ` y ) ) )
9286, 88, 90, 91syl3anc 1268 . . . . . . . . . . . . . . . . . 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 10542 . . . . . . . . . . . . . . . . 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 10197 . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . . . . 20 |- ( M ` A ) = ( (toOMeas ` R ) ` A )
9726adantr 467 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. X ) -> Q e. V )
9827adantr 467 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. X ) -> R : Q --> ( 0 [,] +oo ) )
99 omsfval 29118 . . . . . . . . . . . . . . . . . . . . 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 1268 . . . . . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . . . 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 4412 . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . 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 535 . . . . . . . . . . . . . 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 11717 . . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
108 xrltso 11440 . . . . . . . . . . . . . . . . . . 19 |- < Or RR*
109 soss 4773 . . . . . . . . . . . . . . . . . . 19 |- ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
110107, 108, 109mp2 9 . . . . . . . . . . . . . . . . . 18 |- < Or ( 0 [,] +oo )
111 biid 240 . . . . . . . . . . . . . . . . . 18 |- ( < Or ( 0 [,] +oo ) <-> < Or ( 0 [,] +oo ) )
112110, 111mpbi 212 . . . . . . . . . . . . . . . . 17 |- < Or ( 0 [,] +oo )
113112a1i 11 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. X ) -> < Or ( 0 [,] +oo ) )
114 omscl 29119 . . . . . . . . . . . . . . . . . 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 1268 . . . . . . . . . . . . . . . . 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 28340 . . . . . . . . . . . . . . . . 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 8006 . . . . . . . . . . . . . . 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 431 . . . . . . . . . . . . . 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 1267 . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . . . . 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 28850 . . . . . . . . . . . . . . . . . . 19 |- Σ* w e. x ( R ` w ) e. _V
123121, 122elrnmpti 5085 . . . . . . . . . . . . . . . . . 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 701 . . . . . . . . . . . . . . . . 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 2942 . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . 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 1718 . . . . . . . . . . . . . . 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 2743 . . . . . . . . . . . . . . 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 3067 . . . . . . . . . . . . . . 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 281 . . . . . . . . . . . . . 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 4405 . . . . . . . . . . . . . . . . . 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 25 . . . . . . . . . . . . . . . . . 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 219 . . . . . . . . . . . . . . . . 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 431 . . . . . . . . . . . . . . . 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 1776 . . . . . . . . . . . . . . 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 2855 . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . 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 3511 . . . . . . . . . . . . . 14 |- { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } C_ { z e. ~P dom R | z ~<_ om }
142 rexss 3496 . . . . . . . . . . . . . 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 4206 . . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> U. z = U. x )
145144sseq2d 3460 . . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( A C_ U. z <-> A C_ U. x ) )
146 breq1 4405 . . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( z ~<_ om <-> x ~<_ om ) )
147145, 146anbi12d 717 . . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( A C_ U. z /\ z ~<_ om ) <-> ( A C_ U. x /\ x ~<_ om ) ) )
148147elrab 3196 . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . 17 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } -> ( A C_ U. x /\ x ~<_ om ) )
150149simpld 461 . . . . . . . . . . . . . . . 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 568 . . . . . . . . . . . . . 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 2861 . . . . . . . . . . . . 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 221 . . . . . . . . . . . 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 436 . . . . . . . . . 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 2788 . . . . . . . . 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 4206 . . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> U. x = U. ( g ` y ) )
159158sseq2d 3460 . . . . . . . . . . . 12 |- ( x = ( g ` y ) -> ( A C_ U. x <-> A C_ U. ( g ` y ) ) )
160 esumeq1 28855 . . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> Σ* w e. x ( R ` w ) = Σ* w e. ( g ` y ) ( R ` w ) )
161160breq1d 4412 . . . . . . . . . . . 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 717 . . . . . . . . . . 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 8918 . . . . . . . . . 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 431 . . . . . . . . 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 667 . . . . . . . 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 732 . . . . . . . . . . . . . 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 2802 . . . . . . . . . . . . . . . . . 18 |- ( ph -> A. y e. X A C_ U. dom R )
168 iunss 4319 . . . . . . . . . . . . . . . . . 18 |- ( U_ y e. X A C_ U. dom R <-> A. y e. X A C_ U. dom R )
169167, 168sylibr 216 . . . . . . . . . . . . . . . . 17 |- ( ph -> U_ y e. X A C_ U. dom R )
17044ralrimiva 2802 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. y e. X A e. _V )
171 iunexg 6769 . . . . . . . . . . . . . . . . . . 19 |- ( ( X e. _V /\ A. y e. X A e. _V ) -> U_ y e. X A e. _V )
17211, 170, 171syl2anc 667 . . . . . . . . . . . . . . . . . 18 |- ( ph -> U_ y e. X A e. _V )
173 elpwg 3959 . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . 16 |- ( ph -> U_ y e. X A e. ~P U. dom R )
17632, 175ffvelrnd 6023 . . . . . . . . . . . . . . 15 |- ( ph -> ( M ` U_ y e. X A ) e. ( 0 [,] +oo ) )
177107, 176sseldi 3430 . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . . 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 6138 . . . . . . . . . . . . . . . . 17 |- ( ( g : X --> { z e. ~P dom R | z ~<_ om } /\ X e. _V ) -> g e. _V )
182179, 180, 181syl2anc 667 . . . . . . . . . . . . . . . 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 6725 . . . . . . . . . . . . . . . 16 |- ( g e. _V -> ran g e. _V )
184 uniexg 6588 . . . . . . . . . . . . . . . 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 778 . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> R : Q --> ( 0 [,] +oo ) )
188 frn 5735 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ { z e. ~P dom R | z ~<_ om } )
189 ssrab2 3514 . . . . . . . . . . . . . . . . . . . . . . . 24 |- { z e. ~P dom R | z ~<_ om } C_ ~P dom R
190188, 189syl6ss 3444 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
191190unissd 4222 . . . . . . . . . . . . . . . . . . . . . 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 3478 . . . . . . . . . . . . . . . . . . . . 21 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> U. ran g C_ dom R )
194193adantl 468 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ dom R )
19536adantr 467 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> dom R = Q )
196194, 195sseqtrd 3468 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ Q )
197196sselda 3432 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> c e. Q )
198187, 197ffvelrnd 6023 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> ( R ` c ) e. ( 0 [,] +oo ) )
199198ralrimiva 2802 . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . 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 2592 . . . . . . . . . . . . . . . 16 |- F/_ c U. ran g
202201esumcl 28851 . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . 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 3430 . . . . . . . . . . . . 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 779 . . . . . . . . . . . . . . 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 9690 . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . 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 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> e e. RR* )
209206, 208xaddcld 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> (Σ* y e. X ( M ` A ) +e e ) e. RR* )
210188ad2antlr 733 . . . . . . . . . . . . . . . . . . . . . 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 3440 . . . . . . . . . . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
213 sspwuni 4367 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ ~P dom R <-> U. ran g C_ dom R )
214212, 213sylib 200 . . . . . . . . . . . . . . . . . . . . . 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 5728 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> g Fn X )
217216ad2antlr 733 . . . . . . . . . . . . . . . . . . . . . . 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 28297 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g Fn X /\ X ~<_ om ) -> g ~<_ om )
220 rnct 28300 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( g ~<_ om -> ran g ~<_ om )
221219, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( g Fn X /\ X ~<_ om ) -> ran g ~<_ om )
222 dfss3 3422 . . . . . . . . . . . . . . . . . . . . . . . . . 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 198 . . . . . . . . . . . . . . . . . . . . . . . . 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 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = w -> ( z ~<_ om <-> w ~<_ om ) )
225224elrab 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. { z e. ~P dom R | z ~<_ om } <-> ( w e. ~P dom R /\ w ~<_ om ) )
226225simprbi 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( w e. { z e. ~P dom R | z ~<_ om } -> w ~<_ om )
227226ralimi 2781 . . . . . . . . . . . . . . . . . . . . . . . . 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 9000 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran g ~<_ om /\ A. w e. ran g w ~<_ om ) -> U. ran g ~<_ om )
230221, 228, 229syl2an 480 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( g Fn X /\ X ~<_ om ) /\ ran g C_ { z e. ~P dom R | z ~<_ om } ) -> U. ran g ~<_ om )
231217, 218, 210, 230syl21anc 1267 . . . . . . . . . . . . . . . . . . . . . 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 7584 . . . . . . . . . . . . . . . . . . . . . 22 |- ( U. ran g ~<_ om -> U. ran g e. _V )
233 elpwg 3959 . . . . . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A C_ U. ( g ` y ) )
237236ralimi 2781 . . . . . . . . . . . . . . . . . . . . . 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 5888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g ` y ) C_ U. ran g
239238unissi 4221 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- U. ( g ` y ) C_ U. U. ran g
240 sstr 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. ( g ` y ) /\ U. ( g ` y ) C_ U. U. ran g ) -> A C_ U. U. ran g )
241239, 240mpan2 677 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A C_ U. ( g ` y ) -> A C_ U. U. ran g )
242241ralimi 2781 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( A. y e. X A C_ U. ( g ` y ) -> A. y e. X A C_ U. U. ran g )
243 iunss 4319 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( U_ y e. X A C_ U. U. ran g <-> A. y e. X A C_ U. U. ran g )
244242, 243sylibr 216 . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . 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 538 . . . . . . . . . . . . . . . . . . 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 4206 . . . . . . . . . . . . . . . . . . . . . 22 |- ( z = U. ran g -> U. z = U. U. ran g )
249248sseq2d 3460 . . . . . . . . . . . . . . . . . . . . 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 4405 . . . . . . . . . . . . . . . . . . . . 21 |- ( z = U. ran g -> ( z ~<_ om <-> U. ran g ~<_ om ) )
251249, 250anbi12d 717 . . . . . . . . . . . . . . . . . . . 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 3196 . . . . . . . . . . . . . . . . . . 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 216 . . . . . . . . . . . . . . . . . 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 5865 . . . . . . . . . . . . . . . . . . 19 |- ( c = w -> ( R ` c ) = ( R ` w ) )
255254cbvesumv 28864 . . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) = Σ* w e. U. ran g ( R ` w )
256 esumeq1 28855 . . . . . . . . . . . . . . . . . . . 20 |- ( x = U. ran g -> Σ* w e. x ( R ` w ) = Σ* w e. U. ran g ( R ` w ) )
257256eqeq2d 2461 . . . . . . . . . . . . . . . . . . 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 3150 . . . . . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . . . . . 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 28850 . . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) e. _V
261 eqid 2451 . . . . . . . . . . . . . . . . . . 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 5081 . . . . . . . . . . . . . . . . . 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 216 . . . . . . . . . . . . . . . 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 29119 . . . . . . . . . . . . . . . . . . . 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 1268 . . . . . . . . . . . . . . . . . . 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 28340 . . . . . . . . . . . . . . . . . . 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 8005 . . . . . . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . . . . 20 |- ( M ` U_ y e. X A ) = ( (toOMeas ` R ) ` U_ y e. X A )
272169, 37sseqtrd 3468 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U_ y e. X A C_ U. Q )
273 omsfval 29118 . . . . . . . . . . . . . . . . . . . . 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 1268 . . . . . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . . . 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 4414 . . . . . . . . . . . . . . . . . 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 296 . . . . . . . . . . . . . . . . 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 238 . . . . . . . . . . . . . . . 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 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 ) /\ Σ* 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 240 . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . 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 9699 . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . 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 1761 . . . . . . . . . . . . . . . . . . 19 |- F/ y g : X --> { z e. ~P dom R | z ~<_ om }
28622, 285nfan 2011 . . . . . . . . . . . . . . . . . 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 2769 . . . . . . . . . . . . . . . . . 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 2011 . . . . . . . . . . . . . . . . 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 780 . . . . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . 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 736 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> R : Q --> ( 0 [,] +oo ) )
293 simpllr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> y e. X )
295293, 294ffvelrnd 6023 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3430 . . . . . . . . . . . . . . . . . . . . . . . . 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 3961 . . . . . . . . . . . . . . . . . . . . . . . 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 3468 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ Q )
300 simpr 463 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. ( g ` y ) )
301299, 300sseldd 3433 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. Q )
302292, 301ffvelrnd 6023 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( R ` w ) e. ( 0 [,] +oo ) )
303302ralrimiva 2802 . . . . . . . . . . . . . . . . . . . 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 5875 . . . . . . . . . . . . . . . . . . . . 21 |- ( g ` y ) e. _V
305 nfcv 2592 . . . . . . . . . . . . . . . . . . . . . 22 |- F/_ w ( g ` y )
306305esumcl 28851 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( g ` y )