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 φ Q V
oms.r φ R : Q 0 +∞
omssubaddlem.a φ A Q
omssubaddlem.m φ M A
omssubaddlem.e φ E +
Assertion omssubaddlem φ x z 𝒫 dom R | A z z ω * w x R w < M A + E

Proof

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