Metamath Proof Explorer


Theorem nulmbl2

Description: A set of outer measure zero is measurable. The term "outer measure zero" here is slightly different from "nullset/negligible set"; a nullset has vol* ( A ) = 0 while "outer measure zero" means that for any x there is a y containing A with volume less than x . Assuming AC, these notions are equivalent (because the intersection of all such y is a nullset) but in ZF this is a strictly weaker notion. Proposition 563Gb of Fremlin5 p. 193. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion nulmbl2 x + y dom vol A y vol * y x A dom vol

Proof

Step Hyp Ref Expression
1 1rp 1 +
2 1 ne0ii +
3 r19.2z + x + y dom vol A y vol * y x x + y dom vol A y vol * y x
4 2 3 mpan x + y dom vol A y vol * y x x + y dom vol A y vol * y x
5 simprl y dom vol A y vol * y x A y
6 mblss y dom vol y
7 6 adantr y dom vol A y vol * y x y
8 5 7 sstrd y dom vol A y vol * y x A
9 8 rexlimiva y dom vol A y vol * y x A
10 9 rexlimivw x + y dom vol A y vol * y x A
11 4 10 syl x + y dom vol A y vol * y x A
12 inss1 z A z
13 elpwi z 𝒫 z
14 13 adantr z 𝒫 vol * z z
15 simpr z 𝒫 vol * z vol * z
16 ovolsscl z A z z vol * z vol * z A
17 12 14 15 16 mp3an2i z 𝒫 vol * z vol * z A
18 difssd z 𝒫 vol * z z A z
19 ovolsscl z A z z vol * z vol * z A
20 18 14 15 19 syl3anc z 𝒫 vol * z vol * z A
21 17 20 readdcld z 𝒫 vol * z vol * z A + vol * z A
22 21 ad2antrr z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A + vol * z A
23 15 ad2antrr z 𝒫 vol * z x + y dom vol A y vol * y x vol * z
24 difssd z 𝒫 vol * z x + y dom vol A y vol * y x y A y
25 7 adantl z 𝒫 vol * z x + y dom vol A y vol * y x y
26 rpre x + x
27 26 ad2antlr z 𝒫 vol * z x + y dom vol A y vol * y x x
28 simprrr z 𝒫 vol * z x + y dom vol A y vol * y x vol * y x
29 ovollecl y x vol * y x vol * y
30 25 27 28 29 syl3anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * y
31 ovolsscl y A y y vol * y vol * y A
32 24 25 30 31 syl3anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * y A
33 23 32 readdcld z 𝒫 vol * z x + y dom vol A y vol * y x vol * z + vol * y A
34 23 27 readdcld z 𝒫 vol * z x + y dom vol A y vol * y x vol * z + x
35 17 ad2antrr z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A
36 20 ad2antrr z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A
37 inss1 z y z
38 14 ad2antrr z 𝒫 vol * z x + y dom vol A y vol * y x z
39 ovolsscl z y z z vol * z vol * z y
40 37 38 23 39 mp3an2i z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y
41 difssd z 𝒫 vol * z x + y dom vol A y vol * y x z y z
42 ovolsscl z y z z vol * z vol * z y
43 41 38 23 42 syl3anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y
44 43 32 readdcld z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y + vol * y A
45 simprrl z 𝒫 vol * z x + y dom vol A y vol * y x A y
46 sslin A y z A z y
47 45 46 syl z 𝒫 vol * z x + y dom vol A y vol * y x z A z y
48 37 38 sstrid z 𝒫 vol * z x + y dom vol A y vol * y x z y
49 ovolss z A z y z y vol * z A vol * z y
50 47 48 49 syl2anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A vol * z y
51 38 ssdifssd z 𝒫 vol * z x + y dom vol A y vol * y x z y
52 25 ssdifssd z 𝒫 vol * z x + y dom vol A y vol * y x y A
53 51 52 unssd z 𝒫 vol * z x + y dom vol A y vol * y x z y y A
54 ovolun z y vol * z y y A vol * y A vol * z y y A vol * z y + vol * y A
55 51 43 52 32 54 syl22anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y y A vol * z y + vol * y A
56 ovollecl z y y A vol * z y + vol * y A vol * z y y A vol * z y + vol * y A vol * z y y A
57 53 44 55 56 syl3anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y y A
58 ssun1 z z y
59 undif1 z y y = z y
60 58 59 sseqtrri z z y y
61 ssdif z z y y z A z y y A
62 60 61 ax-mp z A z y y A
63 difundir z y y A = z y A y A
64 62 63 sseqtri z A z y A y A
65 difun1 z y A = z y A
66 ssequn2 A y y A = y
67 45 66 sylib z 𝒫 vol * z x + y dom vol A y vol * y x y A = y
68 67 difeq2d z 𝒫 vol * z x + y dom vol A y vol * y x z y A = z y
69 65 68 eqtr3id z 𝒫 vol * z x + y dom vol A y vol * y x z y A = z y
70 69 uneq1d z 𝒫 vol * z x + y dom vol A y vol * y x z y A y A = z y y A
71 64 70 sseqtrid z 𝒫 vol * z x + y dom vol A y vol * y x z A z y y A
72 ovolss z A z y y A z y y A vol * z A vol * z y y A
73 71 53 72 syl2anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A vol * z y y A
74 36 57 44 73 55 letrd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A vol * z y + vol * y A
75 35 36 40 44 50 74 le2addd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A + vol * z A vol * z y + vol * z y + vol * y A
76 simprl z 𝒫 vol * z x + y dom vol A y vol * y x y dom vol
77 mblsplit y dom vol z vol * z vol * z = vol * z y + vol * z y
78 76 38 23 77 syl3anc z 𝒫 vol * z x + y dom vol A y vol * y x vol * z = vol * z y + vol * z y
79 78 oveq1d z 𝒫 vol * z x + y dom vol A y vol * y x vol * z + vol * y A = vol * z y + vol * z y + vol * y A
80 40 recnd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y
81 43 recnd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y
82 32 recnd z 𝒫 vol * z x + y dom vol A y vol * y x vol * y A
83 80 81 82 addassd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z y + vol * z y + vol * y A = vol * z y + vol * z y + vol * y A
84 79 83 eqtrd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z + vol * y A = vol * z y + vol * z y + vol * y A
85 75 84 breqtrrd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A + vol * z A vol * z + vol * y A
86 difss y A y
87 ovolss y A y y vol * y A vol * y
88 86 25 87 sylancr z 𝒫 vol * z x + y dom vol A y vol * y x vol * y A vol * y
89 32 30 27 88 28 letrd z 𝒫 vol * z x + y dom vol A y vol * y x vol * y A x
90 32 27 23 89 leadd2dd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z + vol * y A vol * z + x
91 22 33 34 85 90 letrd z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A + vol * z A vol * z + x
92 91 rexlimdvaa z 𝒫 vol * z x + y dom vol A y vol * y x vol * z A + vol * z A vol * z + x
93 92 ralimdva z 𝒫 vol * z x + y dom vol A y vol * y x x + vol * z A + vol * z A vol * z + x
94 93 impcom x + y dom vol A y vol * y x z 𝒫 vol * z x + vol * z A + vol * z A vol * z + x
95 21 adantl x + y dom vol A y vol * y x z 𝒫 vol * z vol * z A + vol * z A
96 95 rexrd x + y dom vol A y vol * y x z 𝒫 vol * z vol * z A + vol * z A *
97 simprr x + y dom vol A y vol * y x z 𝒫 vol * z vol * z
98 xralrple vol * z A + vol * z A * vol * z vol * z A + vol * z A vol * z x + vol * z A + vol * z A vol * z + x
99 96 97 98 syl2anc x + y dom vol A y vol * y x z 𝒫 vol * z vol * z A + vol * z A vol * z x + vol * z A + vol * z A vol * z + x
100 94 99 mpbird x + y dom vol A y vol * y x z 𝒫 vol * z vol * z A + vol * z A vol * z
101 100 expr x + y dom vol A y vol * y x z 𝒫 vol * z vol * z A + vol * z A vol * z
102 101 ralrimiva x + y dom vol A y vol * y x z 𝒫 vol * z vol * z A + vol * z A vol * z
103 ismbl2 A dom vol A z 𝒫 vol * z vol * z A + vol * z A vol * z
104 11 102 103 sylanbrc x + y dom vol A y vol * y x A dom vol