Metamath Proof Explorer

Theorem omssubaddlem

Description: For any small margin E , we can find a covering approaching the outer measure of a set A by that margin. (Contributed by Thierry Arnoux, 18-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses oms.m 
|- M = ( toOMeas ` R )
oms.o 
|- ( ph -> Q e. V )
oms.r 
|- ( ph -> R : Q --> ( 0 [,] +oo ) )
omssubaddlem.a 
|- ( ph -> A C_ U. Q )
omssubaddlem.m 
|- ( ph -> ( M ` A ) e. RR )
omssubaddlem.e 
|- ( ph -> E e. RR+ )
Assertion omssubaddlem 
|- ( ph -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + E ) )

Proof

Step Hyp Ref Expression
1 oms.m 
 |-  M = ( toOMeas ` R )
2 oms.o 
 |-  ( ph -> Q e. V )
3 oms.r 
 |-  ( ph -> R : Q --> ( 0 [,] +oo ) )
4 omssubaddlem.a 
 |-  ( ph -> A C_ U. Q )
5 omssubaddlem.m 
 |-  ( ph -> ( M ` A ) e. RR )
6 omssubaddlem.e 
 |-  ( ph -> E e. RR+ )
7 6 rpred 
 |-  ( ph -> E e. RR )
8 5 7 readdcld 
 |-  ( ph -> ( ( M ` A ) + E ) e. RR )
9 8 rexrd 
 |-  ( ph -> ( ( M ` A ) + E ) e. RR* )
10 omsf 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
11 2 3 10 syl2anc 
 |-  ( ph -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
12 1 feq1i 
 |-  ( M : ~P U. dom R --> ( 0 [,] +oo ) <-> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
13 11 12 sylibr 
 |-  ( ph -> M : ~P U. dom R --> ( 0 [,] +oo ) )
14 3 fdmd 
 |-  ( ph -> dom R = Q )
15 14 unieqd 
 |-  ( ph -> U. dom R = U. Q )
16 4 15 sseqtrrd 
 |-  ( ph -> A C_ U. dom R )
17 2 uniexd 
 |-  ( ph -> U. Q e. _V )
18 4 17 jca 
 |-  ( ph -> ( A C_ U. Q /\ U. Q e. _V ) )
19 ssexg 
 |-  ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
20 elpwg 
 |-  ( A e. _V -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
21 18 19 20 3syl 
 |-  ( ph -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
22 16 21 mpbird 
 |-  ( ph -> A e. ~P U. dom R )
23 13 22 ffvelrnd 
 |-  ( ph -> ( M ` A ) e. ( 0 [,] +oo ) )
24 elxrge0 
 |-  ( ( M ` A ) e. ( 0 [,] +oo ) <-> ( ( M ` A ) e. RR* /\ 0 <_ ( M ` A ) ) )
25 24 simprbi 
 |-  ( ( M ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( M ` A ) )
26 23 25 syl 
 |-  ( ph -> 0 <_ ( M ` A ) )
27 6 rpge0d 
 |-  ( ph -> 0 <_ E )
28 5 7 26 27 addge0d 
 |-  ( ph -> 0 <_ ( ( M ` A ) + E ) )
29 elxrge0 
 |-  ( ( ( M ` A ) + E ) e. ( 0 [,] +oo ) <-> ( ( ( M ` A ) + E ) e. RR* /\ 0 <_ ( ( M ` A ) + E ) ) )
30 9 28 29 sylanbrc 
 |-  ( ph -> ( ( M ` A ) + E ) e. ( 0 [,] +oo ) )
31 1 fveq1i 
 |-  ( M ` A ) = ( ( toOMeas ` R ) ` A )
32 omsfval 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( ( toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
33 2 3 4 32 syl3anc 
 |-  ( ph -> ( ( toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
34 31 33 syl5req 
 |-  ( ph -> inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) = ( M ` A ) )
35 5 6 ltaddrpd 
 |-  ( ph -> ( M ` A ) < ( ( M ` A ) + E ) )
36 34 35 eqbrtrd 
 |-  ( ph -> inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + E ) )
37 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
38 xrltso 
 |-  < Or RR*
39 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
40 37 38 39 mp2 
 |-  < Or ( 0 [,] +oo )
41 40 a1i 
 |-  ( ph -> < Or ( 0 [,] +oo ) )
42 omscl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
43 2 3 22 42 syl3anc 
 |-  ( ph -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
44 xrge0infss 
 |-  ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -. t < e /\ A. t e. ( 0 [,] +oo ) ( e < t -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < t ) ) )
45 43 44 syl 
 |-  ( ph -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) -. t < e /\ A. t e. ( 0 [,] +oo ) ( e < t -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < t ) ) )
46 41 45 infglb 
 |-  ( ph -> ( ( ( ( M ` A ) + E ) e. ( 0 [,] +oo ) /\ inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + E ) ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + E ) ) )
47 30 36 46 mp2and 
 |-  ( ph -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + E ) )
48 eqid 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) = ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) )
49 esumex 
 |-  sum* w e. x ( R ` w ) e. _V
50 48 49 elrnmpti 
 |-  ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } u = sum* w e. x ( R ` w ) )
51 50 anbi1i 
 |-  ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + E ) ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) )
52 r19.41v 
 |-  ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) )
53 51 52 bitr4i 
 |-  ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + E ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) )
54 53 exbii 
 |-  ( E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + E ) ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) )
55 df-rex 
 |-  ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + E ) <-> E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + E ) ) )
56 rexcom4 
 |-  ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) )
57 54 55 56 3bitr4i 
 |-  ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + E ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) )
58 breq1 
 |-  ( u = sum* w e. x ( R ` w ) -> ( u < ( ( M ` A ) + E ) <-> sum* w e. x ( R ` w ) < ( ( M ` A ) + E ) ) )
59 58 biimpa 
 |-  ( ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) -> sum* w e. x ( R ` w ) < ( ( M ` A ) + E ) )
60 59 exlimiv 
 |-  ( E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) -> sum* w e. x ( R ` w ) < ( ( M ` A ) + E ) )
61 60 reximi 
 |-  ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } E. u ( u = sum* w e. x ( R ` w ) /\ u < ( ( M ` A ) + E ) ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + E ) )
62 57 61 sylbi 
 |-  ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* w e. x ( R ` w ) ) u < ( ( M ` A ) + E ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + E ) )
63 47 62 syl 
 |-  ( ph -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* w e. x ( R ` w ) < ( ( M ` A ) + E ) )