nulmbl2 - Metamath Proof Explorer

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

Theorem nulmbl2 19384

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 10572	. . . . 5
2		ne0i 3594	. . . . 5
3	1, 2	ax-mp 8	. . . 4
4		r19.2z 3677	. . . 4 $/\$ $/\$ $/\$
5	3, 4	mpan 652	. . 3 $/\$ $/\$
6		simprl 733	. . . . . 6 $/\$ $/\$
7		mblss 19380	. . . . . . 7
8	7	adantr 452	. . . . . 6 $/\$ $/\$
9	6, 8	sstrd 3318	. . . . 5 $/\$ $/\$
10	9	rexlimiva 2785	. . . 4 $/\$
11	10	rexlimivw 2786	. . 3 $/\$
12	5, 11	syl 16	. 2 $/\$
13		inss1 3521	. . . . . . . . . . . . 13
14	13	a1i 11	. . . . . . . . . . . 12 $/\$
15		elpwi 3767	. . . . . . . . . . . . 13
16	15	adantr 452	. . . . . . . . . . . 12 $/\$
17		simpr 448	. . . . . . . . . . . 12 $/\$
18		ovolsscl 19335	. . . . . . . . . . . 12 $/\$ $/\$
19	14, 16, 17, 18	syl3anc 1184	. . . . . . . . . . 11 $/\$
20		difssd 3435	. . . . . . . . . . . 12 $/\$ $\$
21		ovolsscl 19335	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$
22	20, 16, 17, 21	syl3anc 1184	. . . . . . . . . . 11 $/\$ $\$
23	19, 22	readdcld 9071	. . . . . . . . . 10 $/\$ $\$
24	23	ad2antrr 707	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
25	17	ad2antrr 707	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		difssd 3435	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
27	8	adantl 453	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
28		rpre 10574	. . . . . . . . . . . . 13
29	28	ad2antlr 708	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
30		simprrr 742	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
31		ovollecl 19332	. . . . . . . . . . . 12 $/\$ $/\$
32	27, 29, 30, 31	syl3anc 1184	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33		ovolsscl 19335	. . . . . . . . . . 11 $\$ $/\$ $/\$ $\$
34	26, 27, 32, 33	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
35	25, 34	readdcld 9071	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
36	25, 29	readdcld 9071	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
37	19	ad2antrr 707	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
38	22	ad2antrr 707	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		inss1 3521	. . . . . . . . . . . . 13
40	39	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
41	16	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
42		ovolsscl 19335	. . . . . . . . . . . 12 $/\$ $/\$
43	40, 41, 25, 42	syl3anc 1184	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
44		difssd 3435	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45		ovolsscl 19335	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$
46	44, 41, 25, 45	syl3anc 1184	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
47	46, 34	readdcld 9071	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
48		simprrl 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
49		sslin 3527	. . . . . . . . . . . . 13
50	48, 49	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
51	39, 41	syl5ss 3319	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
52		ovolss 19334	. . . . . . . . . . . 12 $/\$
53	50, 51, 52	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
54	41	ssdifssd 3445	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	27	ssdifssd 3445	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
56	54, 55	unssd 3483	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
57		ovolun 19348	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
58	54, 46, 55, 34, 57	syl22anc 1185	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
59		ovollecl 19332	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
60	56, 47, 58, 59	syl3anc 1184	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
61		ssun1 3470	. . . . . . . . . . . . . . . . 17
62		undif1 3663	. . . . . . . . . . . . . . . . 17 $\$
63	61, 62	sseqtr4i 3341	. . . . . . . . . . . . . . . 16 $\$
64		ssdif 3442	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
65	63, 64	ax-mp 8	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
66		difundir 3554	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
67	65, 66	sseqtri 3340	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
68		difun1 3561	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
69		ssequn2 3480	. . . . . . . . . . . . . . . . . 18
70	48, 69	sylib 189	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	difeq2d 3425	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
72	68, 71	syl5eqr 2450	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
73	72	uneq1d 3460	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
74	67, 73	syl5sseq 3356	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
75		ovolss 19334	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
76	74, 56, 75	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
77	38, 60, 47, 76, 58	letrd 9183	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
78	37, 38, 43, 47, 53, 77	le2addd 9600	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
79		simprl 733	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
80		mblsplit 19381	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
81	79, 41, 25, 80	syl3anc 1184	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
82	81	oveq1d 6055	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
83	43	recnd 9070	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	46	recnd 9070	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
85	34	recnd 9070	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
86	83, 84, 85	addassd 9066	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
87	82, 86	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
88	78, 87	breqtrrd 4198	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
89		difss 3434	. . . . . . . . . . . 12 $\$
90		ovolss 19334	. . . . . . . . . . . 12 $\$ $/\$ $\$
91	89, 27, 90	sylancr 645	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	34, 32, 29, 91, 30	letrd 9183	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93	34, 29, 25, 92	leadd2dd 9597	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
94	24, 35, 36, 88, 93	letrd 9183	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
95	94	rexlimdvaa 2791	. . . . . . 7 $/\$ $/\$ $/\$ $\$
96	95	ralimdva 2744	. . . . . 6 $/\$ $/\$ $\$
97	96	impcom 420	. . . . 5 $/\$ $/\$ $/\$ $\$
98	23	adantl 453	. . . . . . 7 $/\$ $/\$ $/\$ $\$
99	98	rexrd 9090	. . . . . 6 $/\$ $/\$ $/\$ $\$
100		simprr 734	. . . . . 6 $/\$ $/\$ $/\$
101		xralrple 10747	. . . . . 6 $\$ $/\$ $\$ $\$
102	99, 100, 101	syl2anc 643	. . . . 5 $/\$ $/\$ $/\$ $\$ $\$
103	97, 102	mpbird 224	. . . 4 $/\$ $/\$ $/\$ $\$
104	103	expr 599	. . 3 $/\$ $/\$ $\$
105	104	ralrimiva 2749	. 2 $/\$ $\$
106		ismbl2 19376	. 2 $/\$ $\$
107	12, 105, 106	sylanbrc 646	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667 $\$ cdif 3277

cun 3278

cin 3279

wss 3280

c0 3588

cpw 3759 class class class wbr 4172

cdm 4837

cfv 5413 (class class class)co 6040

cr 8945

c1 8947

caddc 8949

cxr 9075

cle 9077

crp 10568

covol 19312

cvol 19313

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-sup 7404 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-ioo 10876 df-ico 10878 df-icc 10879 df-fz 11000 df-fl 11157 df-seq 11279 df-exp 11338 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-ovol 19314 df-vol 19315

W3C validator