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 2 uniexd φ Q V
18 4 17 jca φ A Q Q V
19 ssexg A Q Q V A V
20 elpwg A V A 𝒫 dom R A dom R
21 18 19 20 3syl φ A 𝒫 dom R A dom R
22 16 21 mpbird φ A 𝒫 dom R
23 13 22 ffvelrnd φ M A 0 +∞
24 elxrge0 M A 0 +∞ M A * 0 M A
25 24 simprbi M A 0 +∞ 0 M A
26 23 25 syl φ 0 M A
27 6 rpge0d φ 0 E
28 5 7 26 27 addge0d φ 0 M A + E
29 elxrge0 M A + E 0 +∞ M A + E * 0 M A + E
30 9 28 29 sylanbrc φ M A + E 0 +∞
31 1 fveq1i M A = toOMeas R A
32 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 +∞ <
33 2 3 4 32 syl3anc φ toOMeas R A = sup ran x z 𝒫 dom R | A z z ω * w x R w 0 +∞ <
34 31 33 eqtr2id φ sup ran x z 𝒫 dom R | A z z ω * w x R w 0 +∞ < = M A
35 5 6 ltaddrpd φ M A < M A + E
36 34 35 eqbrtrd φ sup ran x z 𝒫 dom R | A z z ω * w x R w 0 +∞ < < M A + E
37 iccssxr 0 +∞ *
38 xrltso < Or *
39 soss 0 +∞ * < Or * < Or 0 +∞
40 37 38 39 mp2 < Or 0 +∞
41 40 a1i φ < Or 0 +∞
42 omscl Q V R : Q 0 +∞ A 𝒫 dom R ran x z 𝒫 dom R | A z z ω * w x R w 0 +∞
43 2 3 22 42 syl3anc φ ran x z 𝒫 dom R | A z z ω * w x R w 0 +∞
44 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
45 43 44 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
46 41 45 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
47 30 36 46 mp2and φ u ran x z 𝒫 dom R | A z z ω * w x R w u < M A + E
48 eqid x z 𝒫 dom R | A z z ω * w x R w = x z 𝒫 dom R | A z z ω * w x R w
49 esumex * w x R w V
50 48 49 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
51 50 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
52 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
53 51 52 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
54 53 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
55 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
56 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
57 54 55 56 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
58 breq1 u = * w x R w u < M A + E * w x R w < M A + E
59 58 biimpa u = * w x R w u < M A + E * w x R w < M A + E
60 59 exlimiv u u = * w x R w u < M A + E * w x R w < M A + E
61 60 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
62 57 61 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
63 47 62 syl φ x z 𝒫 dom R | A z z ω * w x R w < M A + E