nulmbl2 - Metamath Proof Explorer

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

Theorem nulmbl2 21021

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 10998	. . . . 5
2		ne0i 3646	. . . . 5
3	1, 2	ax-mp 5	. . . 4
4		r19.2z 3772	. . . 4 $/\$ $/\$ $/\$
5	3, 4	mpan 670	. . 3 $/\$ $/\$
6		simprl 755	. . . . . 6 $/\$ $/\$
7		mblss 21017	. . . . . . 7
8	7	adantr 465	. . . . . 6 $/\$ $/\$
9	6, 8	sstrd 3369	. . . . 5 $/\$ $/\$
10	9	rexlimiva 2839	. . . 4 $/\$
11	10	rexlimivw 2840	. . 3 $/\$
12	5, 11	syl 16	. 2 $/\$
13		inss1 3573	. . . . . . . . . . . . 13
14	13	a1i 11	. . . . . . . . . . . 12 $/\$
15		elpwi 3872	. . . . . . . . . . . . 13
16	15	adantr 465	. . . . . . . . . . . 12 $/\$
17		simpr 461	. . . . . . . . . . . 12 $/\$
18		ovolsscl 20972	. . . . . . . . . . . 12 $/\$ $/\$
19	14, 16, 17, 18	syl3anc 1218	. . . . . . . . . . 11 $/\$
20		difssd 3487	. . . . . . . . . . . 12 $/\$ $\$
21		ovolsscl 20972	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$
22	20, 16, 17, 21	syl3anc 1218	. . . . . . . . . . 11 $/\$ $\$
23	19, 22	readdcld 9416	. . . . . . . . . 10 $/\$ $\$
24	23	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
25	17	ad2antrr 725	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		difssd 3487	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
27	8	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
28		rpre 11000	. . . . . . . . . . . . 13
29	28	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
30		simprrr 764	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
31		ovollecl 20969	. . . . . . . . . . . 12 $/\$ $/\$
32	27, 29, 30, 31	syl3anc 1218	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33		ovolsscl 20972	. . . . . . . . . . 11 $\$ $/\$ $/\$ $\$
34	26, 27, 32, 33	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
35	25, 34	readdcld 9416	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
36	25, 29	readdcld 9416	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
37	19	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
38	22	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		inss1 3573	. . . . . . . . . . . . 13
40	39	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
41	16	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
42		ovolsscl 20972	. . . . . . . . . . . 12 $/\$ $/\$
43	40, 41, 25, 42	syl3anc 1218	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
44		difssd 3487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45		ovolsscl 20972	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$
46	44, 41, 25, 45	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
47	46, 34	readdcld 9416	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
48		simprrl 763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
49		sslin 3579	. . . . . . . . . . . . 13
50	48, 49	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
51	39, 41	syl5ss 3370	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
52		ovolss 20971	. . . . . . . . . . . 12 $/\$
53	50, 51, 52	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
54	41	ssdifssd 3497	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	27	ssdifssd 3497	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
56	54, 55	unssd 3535	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
57		ovolun 20985	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
58	54, 46, 55, 34, 57	syl22anc 1219	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
59		ovollecl 20969	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
60	56, 47, 58, 59	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
61		ssun1 3522	. . . . . . . . . . . . . . . . 17
62		undif1 3757	. . . . . . . . . . . . . . . . 17 $\$
63	61, 62	sseqtr4i 3392	. . . . . . . . . . . . . . . 16 $\$
64		ssdif 3494	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
65	63, 64	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
66		difundir 3606	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
67	65, 66	sseqtri 3391	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
68		difun1 3613	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
69		ssequn2 3532	. . . . . . . . . . . . . . . . . 18
70	48, 69	sylib 196	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	difeq2d 3477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
72	68, 71	syl5eqr 2489	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
73	72	uneq1d 3512	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
74	67, 73	syl5sseq 3407	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
75		ovolss 20971	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
76	74, 56, 75	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
77	38, 60, 47, 76, 58	letrd 9531	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
78	37, 38, 43, 47, 53, 77	le2addd 9960	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
79		simprl 755	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
80		mblsplit 21018	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
81	79, 41, 25, 80	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
82	81	oveq1d 6109	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
83	43	recnd 9415	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	46	recnd 9415	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
85	34	recnd 9415	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
86	83, 84, 85	addassd 9411	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
87	82, 86	eqtrd 2475	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
88	78, 87	breqtrrd 4321	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
89		difss 3486	. . . . . . . . . . . 12 $\$
90		ovolss 20971	. . . . . . . . . . . 12 $\$ $/\$ $\$
91	89, 27, 90	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	34, 32, 29, 91, 30	letrd 9531	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93	34, 29, 25, 92	leadd2dd 9957	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
94	24, 35, 36, 88, 93	letrd 9531	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
95	94	rexlimdvaa 2845	. . . . . . 7 $/\$ $/\$ $/\$ $\$
96	95	ralimdva 2797	. . . . . 6 $/\$ $/\$ $\$
97	96	impcom 430	. . . . 5 $/\$ $/\$ $/\$ $\$
98	23	adantl 466	. . . . . . 7 $/\$ $/\$ $/\$ $\$
99	98	rexrd 9436	. . . . . 6 $/\$ $/\$ $/\$ $\$
100		simprr 756	. . . . . 6 $/\$ $/\$ $/\$
101		xralrple 11178	. . . . . 6 $\$ $/\$ $\$ $\$
102	99, 100, 101	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $\$ $\$
103	97, 102	mpbird 232	. . . 4 $/\$ $/\$ $/\$ $\$
104	103	expr 615	. . 3 $/\$ $/\$ $\$
105	104	ralrimiva 2802	. 2 $/\$ $\$
106		ismbl2 21013	. 2 $/\$ $\$
107	12, 105, 106	sylanbrc 664	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1369

wcel 1756

wne 2609

wral 2718

wrex 2719 $\$ cdif 3328

cun 3329

cin 3330

wss 3331

c0 3640

cpw 3863 class class class wbr 4295

cdm 4843

cfv 5421 (class class class)co 6094

cr 9284

c1 9286

caddc 9288

cxr 9420

cle 9422

crp 10994

covol 20949

cvol 20950

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4416 ax-nul 4424 ax-pow 4473 ax-pr 4534 ax-un 6375 ax-cnex 9341 ax-resscn 9342 ax-1cn 9343 ax-icn 9344 ax-addcl 9345 ax-addrcl 9346 ax-mulcl 9347 ax-mulrcl 9348 ax-mulcom 9349 ax-addass 9350 ax-mulass 9351 ax-distr 9352 ax-i2m1 9353 ax-1ne0 9354 ax-1rid 9355 ax-rnegex 9356 ax-rrecex 9357 ax-cnre 9358 ax-pre-lttri 9359 ax-pre-lttrn 9360 ax-pre-ltadd 9361 ax-pre-mulgt0 9362 ax-pre-sup 9363

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2571 df-ne 2611 df-nel 2612 df-ral 2723 df-rex 2724 df-reu 2725 df-rmo 2726 df-rab 2727 df-v 2977 df-sbc 3190 df-csb 3292 df-dif 3334 df-un 3336 df-in 3338 df-ss 3345 df-pss 3347 df-nul 3641 df-if 3795 df-pw 3865 df-sn 3881 df-pr 3883 df-tp 3885 df-op 3887 df-uni 4095 df-iun 4176 df-br 4296 df-opab 4354 df-mpt 4355 df-tr 4389 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4849 df-rel 4850 df-cnv 4851 df-co 4852 df-dm 4853 df-rn 4854 df-res 4855 df-ima 4856 df-iota 5384 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-riota 6055 df-ov 6097 df-oprab 6098 df-mpt2 6099 df-om 6480 df-1st 6580 df-2nd 6581 df-recs 6835 df-rdg 6869 df-er 7104 df-map 7219 df-en 7314 df-dom 7315 df-sdom 7316 df-sup 7694 df-pnf 9423 df-mnf 9424 df-xr 9425 df-ltxr 9426 df-le 9427 df-sub 9600 df-neg 9601 df-div 9997 df-nn 10326 df-2 10383 df-3 10384 df-n0 10583 df-z 10650 df-uz 10865 df-q 10957 df-rp 10995 df-ioo 11307 df-ico 11309 df-icc 11310 df-fz 11441 df-fl 11645 df-seq 11810 df-exp 11869 df-cj 12591 df-re 12592 df-im 12593 df-sqr 12727 df-abs 12728 df-ovol 20951 df-vol 20952

This theorem is referenced by: (None)

W3C validator