nulmbl2 - Metamath Proof Explorer

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

Theorem nulmbl2 22364

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.

Step	Hyp	Ref	Expression
1		1rp 11295	. . . . 5
2	1	ne0ii 3765	. . . 4
3		r19.2z 3883	. . . 4 $/\$ $/\$ $/\$
4	2, 3	mpan 674	. . 3 $/\$ $/\$
5		simprl 762	. . . . . 6 $/\$ $/\$
6		mblss 22359	. . . . . . 7
7	6	adantr 466	. . . . . 6 $/\$ $/\$
8	5, 7	sstrd 3471	. . . . 5 $/\$ $/\$
9	8	rexlimiva 2911	. . . 4 $/\$
10	9	rexlimivw 2912	. . 3 $/\$
11	4, 10	syl 17	. 2 $/\$
12		inss1 3679	. . . . . . . . . . . . 13
13	12	a1i 11	. . . . . . . . . . . 12 $/\$
14		elpwi 3985	. . . . . . . . . . . . 13
15	14	adantr 466	. . . . . . . . . . . 12 $/\$
16		simpr 462	. . . . . . . . . . . 12 $/\$
17		ovolsscl 22313	. . . . . . . . . . . 12 $/\$ $/\$
18	13, 15, 16, 17	syl3anc 1264	. . . . . . . . . . 11 $/\$
19		difssd 3590	. . . . . . . . . . . 12 $/\$ $\$
20		ovolsscl 22313	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$
21	19, 15, 16, 20	syl3anc 1264	. . . . . . . . . . 11 $/\$ $\$
22	18, 21	readdcld 9659	. . . . . . . . . 10 $/\$ $\$
23	22	ad2antrr 730	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
24	16	ad2antrr 730	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
25		difssd 3590	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
26	7	adantl 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
27		rpre 11297	. . . . . . . . . . . . 13
28	27	ad2antlr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
29		simprrr 773	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
30		ovollecl 22310	. . . . . . . . . . . 12 $/\$ $/\$
31	26, 28, 29, 30	syl3anc 1264	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
32		ovolsscl 22313	. . . . . . . . . . 11 $\$ $/\$ $/\$ $\$
33	25, 26, 31, 32	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	24, 33	readdcld 9659	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
35	24, 28	readdcld 9659	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
36	18	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
37	21	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
38		inss1 3679	. . . . . . . . . . . . 13
39	38	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
40	15	ad2antrr 730	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
41		ovolsscl 22313	. . . . . . . . . . . 12 $/\$ $/\$
42	39, 40, 24, 41	syl3anc 1264	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
43		difssd 3590	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
44		ovolsscl 22313	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$
45	43, 40, 24, 44	syl3anc 1264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46	45, 33	readdcld 9659	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
47		simprrl 772	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
48		sslin 3685	. . . . . . . . . . . . 13
49	47, 48	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
50	38, 40	syl5ss 3472	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
51		ovolss 22312	. . . . . . . . . . . 12 $/\$
52	49, 50, 51	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
53	40	ssdifssd 3600	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	26	ssdifssd 3600	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	53, 54	unssd 3639	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
56		ovolun 22326	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
57	53, 45, 54, 33, 56	syl22anc 1265	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
58		ovollecl 22310	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
59	55, 46, 57, 58	syl3anc 1264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
60		ssun1 3626	. . . . . . . . . . . . . . . . 17
61		undif1 3867	. . . . . . . . . . . . . . . . 17 $\$
62	60, 61	sseqtr4i 3494	. . . . . . . . . . . . . . . 16 $\$
63		ssdif 3597	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
65		difundir 3723	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
66	64, 65	sseqtri 3493	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
67		difun1 3730	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
68		ssequn2 3636	. . . . . . . . . . . . . . . . . 18
69	47, 68	sylib 199	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
70	69	difeq2d 3580	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
71	67, 70	syl5eqr 2475	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
72	71	uneq1d 3616	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
73	66, 72	syl5sseq 3509	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
74		ovolss 22312	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
75	73, 55, 74	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
76	37, 59, 46, 75, 57	letrd 9781	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
77	36, 37, 42, 46, 52, 76	le2addd 10221	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
78		simprl 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
79		mblsplit 22360	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
80	78, 40, 24, 79	syl3anc 1264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
81	80	oveq1d 6311	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
82	42	recnd 9658	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
83	45	recnd 9658	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
84	33	recnd 9658	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
85	82, 83, 84	addassd 9654	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
86	81, 85	eqtrd 2461	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
87	77, 86	breqtrrd 4443	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
88		difss 3589	. . . . . . . . . . . 12 $\$
89		ovolss 22312	. . . . . . . . . . . 12 $\$ $/\$ $\$
90	88, 26, 89	sylancr 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
91	33, 31, 28, 90, 29	letrd 9781	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	33, 28, 24, 91	leadd2dd 10217	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93	23, 34, 35, 87, 92	letrd 9781	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
94	93	rexlimdvaa 2916	. . . . . . 7 $/\$ $/\$ $/\$ $\$
95	94	ralimdva 2831	. . . . . 6 $/\$ $/\$ $\$
96	95	impcom 431	. . . . 5 $/\$ $/\$ $/\$ $\$
97	22	adantl 467	. . . . . . 7 $/\$ $/\$ $/\$ $\$
98	97	rexrd 9679	. . . . . 6 $/\$ $/\$ $/\$ $\$
99		simprr 764	. . . . . 6 $/\$ $/\$ $/\$
100		xralrple 11487	. . . . . 6 $\$ $/\$ $\$ $\$
101	98, 99, 100	syl2anc 665	. . . . 5 $/\$ $/\$ $/\$ $\$ $\$
102	96, 101	mpbird 235	. . . 4 $/\$ $/\$ $/\$ $\$
103	102	expr 618	. . 3 $/\$ $/\$ $\$
104	103	ralrimiva 2837	. 2 $/\$ $\$
105		ismbl2 22355	. 2 $/\$ $\$
106	11, 104, 105	sylanbrc 668	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370

wceq 1437

wcel 1867

wne 2616

wral 2773

wrex 2774 $\$ cdif 3430

cun 3431

cin 3432

wss 3433

c0 3758

cpw 3976 class class class wbr 4417

cdm 4845

cfv 5592 (class class class)co 6296

cr 9527

c1 9529

caddc 9531

cxr 9663

cle 9665

crp 11291

covol 22287

cvol 22289

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605 ax-pre-sup 9606

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-er 7362 df-map 7473 df-en 7569 df-dom 7570 df-sdom 7571 df-sup 7953 df-inf 7954 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-div 10259 df-nn 10599 df-2 10657 df-3 10658 df-n0 10859 df-z 10927 df-uz 11149 df-q 11254 df-rp 11292 df-ioo 11628 df-ico 11630 df-icc 11631 df-fz 11772 df-fl 12014 df-seq 12200 df-exp 12259 df-cj 13130 df-re 13131 df-im 13132 df-sqrt 13266 df-abs 13267 df-ovol 22290 df-vol 22292

This theorem is referenced by: (None)

W3C validator