Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nulmbl2 Unicode version

Theorem nulmbl2 19419
 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 while "outer measure zero" means that for any there is a containing with volume less than . Assuming AC, these notions are equivalent (because the intersection of all such 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.)
Assertion
Ref Expression
nulmbl2
Distinct variable group:   ,,

Proof of Theorem nulmbl2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 1rp 10605 . . . . 5
2 ne0i 3626 . . . . 5
31, 2ax-mp 8 . . . 4
4 r19.2z 3709 . . . 4
53, 4mpan 652 . . 3
6 simprl 733 . . . . . 6
7 mblss 19415 . . . . . . 7
87adantr 452 . . . . . 6
96, 8sstrd 3350 . . . . 5
109rexlimiva 2817 . . . 4
1110rexlimivw 2818 . . 3
125, 11syl 16 . 2
13 inss1 3553 . . . . . . . . . . . . 13
1413a1i 11 . . . . . . . . . . . 12
15 elpwi 3799 . . . . . . . . . . . . 13
1615adantr 452 . . . . . . . . . . . 12
17 simpr 448 . . . . . . . . . . . 12
18 ovolsscl 19370 . . . . . . . . . . . 12
1914, 16, 17, 18syl3anc 1184 . . . . . . . . . . 11
20 difssd 3467 . . . . . . . . . . . 12
21 ovolsscl 19370 . . . . . . . . . . . 12
2220, 16, 17, 21syl3anc 1184 . . . . . . . . . . 11
2319, 22readdcld 9104 . . . . . . . . . 10
2423ad2antrr 707 . . . . . . . . 9
2517ad2antrr 707 . . . . . . . . . 10
26 difssd 3467 . . . . . . . . . . 11
278adantl 453 . . . . . . . . . . 11
28 rpre 10607 . . . . . . . . . . . . 13
2928ad2antlr 708 . . . . . . . . . . . 12
30 simprrr 742 . . . . . . . . . . . 12
31 ovollecl 19367 . . . . . . . . . . . 12
3227, 29, 30, 31syl3anc 1184 . . . . . . . . . . 11
33 ovolsscl 19370 . . . . . . . . . . 11
3426, 27, 32, 33syl3anc 1184 . . . . . . . . . 10
3525, 34readdcld 9104 . . . . . . . . 9
3625, 29readdcld 9104 . . . . . . . . 9
3719ad2antrr 707 . . . . . . . . . . 11
3822ad2antrr 707 . . . . . . . . . . 11
39 inss1 3553 . . . . . . . . . . . . 13
4039a1i 11 . . . . . . . . . . . 12
4116ad2antrr 707 . . . . . . . . . . . 12
42 ovolsscl 19370 . . . . . . . . . . . 12
4340, 41, 25, 42syl3anc 1184 . . . . . . . . . . 11
44 difssd 3467 . . . . . . . . . . . . 13
45 ovolsscl 19370 . . . . . . . . . . . . 13
4644, 41, 25, 45syl3anc 1184 . . . . . . . . . . . 12
4746, 34readdcld 9104 . . . . . . . . . . 11
48 simprrl 741 . . . . . . . . . . . . 13
49 sslin 3559 . . . . . . . . . . . . 13
5048, 49syl 16 . . . . . . . . . . . 12
5139, 41syl5ss 3351 . . . . . . . . . . . 12
52 ovolss 19369 . . . . . . . . . . . 12
5350, 51, 52syl2anc 643 . . . . . . . . . . 11
5441ssdifssd 3477 . . . . . . . . . . . . . 14
5527ssdifssd 3477 . . . . . . . . . . . . . 14
5654, 55unssd 3515 . . . . . . . . . . . . 13
57 ovolun 19383 . . . . . . . . . . . . . 14
5854, 46, 55, 34, 57syl22anc 1185 . . . . . . . . . . . . 13
59 ovollecl 19367 . . . . . . . . . . . . 13
6056, 47, 58, 59syl3anc 1184 . . . . . . . . . . . 12
61 ssun1 3502 . . . . . . . . . . . . . . . . 17
62 undif1 3695 . . . . . . . . . . . . . . . . 17
6361, 62sseqtr4i 3373 . . . . . . . . . . . . . . . 16
64 ssdif 3474 . . . . . . . . . . . . . . . 16
6563, 64ax-mp 8 . . . . . . . . . . . . . . 15
66 difundir 3586 . . . . . . . . . . . . . . 15
6765, 66sseqtri 3372 . . . . . . . . . . . . . 14
68 difun1 3593 . . . . . . . . . . . . . . . 16
69 ssequn2 3512 . . . . . . . . . . . . . . . . . 18
7048, 69sylib 189 . . . . . . . . . . . . . . . . 17
7170difeq2d 3457 . . . . . . . . . . . . . . . 16
7268, 71syl5eqr 2481 . . . . . . . . . . . . . . 15
7372uneq1d 3492 . . . . . . . . . . . . . 14
7467, 73syl5sseq 3388 . . . . . . . . . . . . 13
75 ovolss 19369 . . . . . . . . . . . . 13
7674, 56, 75syl2anc 643 . . . . . . . . . . . 12
7738, 60, 47, 76, 58letrd 9216 . . . . . . . . . . 11
7837, 38, 43, 47, 53, 77le2addd 9633 . . . . . . . . . 10
79 simprl 733 . . . . . . . . . . . . 13
80 mblsplit 19416 . . . . . . . . . . . . 13
8179, 41, 25, 80syl3anc 1184 . . . . . . . . . . . 12
8281oveq1d 6087 . . . . . . . . . . 11
8343recnd 9103 . . . . . . . . . . . 12
8446recnd 9103 . . . . . . . . . . . 12
8534recnd 9103 . . . . . . . . . . . 12
8683, 84, 85addassd 9099 . . . . . . . . . . 11
8782, 86eqtrd 2467 . . . . . . . . . 10
8878, 87breqtrrd 4230 . . . . . . . . 9
89 difss 3466 . . . . . . . . . . . 12
90 ovolss 19369 . . . . . . . . . . . 12
9189, 27, 90sylancr 645 . . . . . . . . . . 11
9234, 32, 29, 91, 30letrd 9216 . . . . . . . . . 10
9334, 29, 25, 92leadd2dd 9630 . . . . . . . . 9
9424, 35, 36, 88, 93letrd 9216 . . . . . . . 8
9594rexlimdvaa 2823 . . . . . . 7
9695ralimdva 2776 . . . . . 6
9796impcom 420 . . . . 5
9823adantl 453 . . . . . . 7
9998rexrd 9123 . . . . . 6
100 simprr 734 . . . . . 6
101 xralrple 10780 . . . . . 6
10299, 100, 101syl2anc 643 . . . . 5
10397, 102mpbird 224 . . . 4
104103expr 599 . . 3
105104ralrimiva 2781 . 2
106 ismbl2 19411 . 2
10712, 105, 106sylanbrc 646 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698   cdif 3309   cun 3310   cin 3311   wss 3312  c0 3620  cpw 3791   class class class wbr 4204   cdm 4869  cfv 5445  (class class class)co 6072  cr 8978  c1 8980   caddc 8982  cxr 9108   cle 9110  crp 10601  covol 19347  cvol 19348 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-cnex 9035  ax-resscn 9036  ax-1cn 9037  ax-icn 9038  ax-addcl 9039  ax-addrcl 9040  ax-mulcl 9041  ax-mulrcl 9042  ax-mulcom 9043  ax-addass 9044  ax-mulass 9045  ax-distr 9046  ax-i2m1 9047  ax-1ne0 9048  ax-1rid 9049  ax-rnegex 9050  ax-rrecex 9051  ax-cnre 9052  ax-pre-lttri 9053  ax-pre-lttrn 9054  ax-pre-ltadd 9055  ax-pre-mulgt0 9056  ax-pre-sup 9057 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4837  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-1st 6340  df-2nd 6341  df-riota 6540  df-recs 6624  df-rdg 6659  df-er 6896  df-map 7011  df-en 7101  df-dom 7102  df-sdom 7103  df-sup 7437  df-pnf 9111  df-mnf 9112  df-xr 9113  df-ltxr 9114  df-le 9115  df-sub 9282  df-neg 9283  df-div 9667  df-nn 9990  df-2 10047  df-3 10048  df-n0 10211  df-z 10272  df-uz 10478  df-q 10564  df-rp 10602  df-ioo 10909  df-ico 10911  df-icc 10912  df-fz 11033  df-fl 11190  df-seq 11312  df-exp 11371  df-cj 11892  df-re 11893  df-im 11894  df-sqr 12028  df-abs 12029  df-ovol 19349  df-vol 19350
 Copyright terms: Public domain W3C validator