nulmbl2 - Metamath Proof Explorer

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

Theorem nulmbl2 22568

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 11329	. . . . 5
2	1	ne0ii 3729	. . . 4
3		r19.2z 3849	. . . 4 $/\$ $/\$ $/\$
4	2, 3	mpan 684	. . 3 $/\$ $/\$
5		simprl 772	. . . . . 6 $/\$ $/\$
6		mblss 22563	. . . . . . 7
7	6	adantr 472	. . . . . 6 $/\$ $/\$
8	5, 7	sstrd 3428	. . . . 5 $/\$ $/\$
9	8	rexlimiva 2868	. . . 4 $/\$
10	9	rexlimivw 2869	. . 3 $/\$
11	4, 10	syl 17	. 2 $/\$
12		inss1 3643	. . . . . . . . . . . . 13
13	12	a1i 11	. . . . . . . . . . . 12 $/\$
14		elpwi 3951	. . . . . . . . . . . . 13
15	14	adantr 472	. . . . . . . . . . . 12 $/\$
16		simpr 468	. . . . . . . . . . . 12 $/\$
17		ovolsscl 22517	. . . . . . . . . . . 12 $/\$ $/\$
18	13, 15, 16, 17	syl3anc 1292	. . . . . . . . . . 11 $/\$
19		difssd 3550	. . . . . . . . . . . 12 $/\$ $\$
20		ovolsscl 22517	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$
21	19, 15, 16, 20	syl3anc 1292	. . . . . . . . . . 11 $/\$ $\$
22	18, 21	readdcld 9688	. . . . . . . . . 10 $/\$ $\$
23	22	ad2antrr 740	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
24	16	ad2antrr 740	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
25		difssd 3550	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
26	7	adantl 473	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
27		rpre 11331	. . . . . . . . . . . . 13
28	27	ad2antlr 741	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
29		simprrr 783	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
30		ovollecl 22514	. . . . . . . . . . . 12 $/\$ $/\$
31	26, 28, 29, 30	syl3anc 1292	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
32		ovolsscl 22517	. . . . . . . . . . 11 $\$ $/\$ $/\$ $\$
33	25, 26, 31, 32	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	24, 33	readdcld 9688	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
35	24, 28	readdcld 9688	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
36	18	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
37	21	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
38		inss1 3643	. . . . . . . . . . . . 13
39	38	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
40	15	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
41		ovolsscl 22517	. . . . . . . . . . . 12 $/\$ $/\$
42	39, 40, 24, 41	syl3anc 1292	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
43		difssd 3550	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
44		ovolsscl 22517	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$
45	43, 40, 24, 44	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46	45, 33	readdcld 9688	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
47		simprrl 782	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
48		sslin 3649	. . . . . . . . . . . . 13
49	47, 48	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
50	38, 40	syl5ss 3429	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
51		ovolss 22516	. . . . . . . . . . . 12 $/\$
52	49, 50, 51	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
53	40	ssdifssd 3560	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	26	ssdifssd 3560	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	53, 54	unssd 3601	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
56		ovolun 22530	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
57	53, 45, 54, 33, 56	syl22anc 1293	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
58		ovollecl 22514	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
59	55, 46, 57, 58	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
60		ssun1 3588	. . . . . . . . . . . . . . . . 17
61		undif1 3833	. . . . . . . . . . . . . . . . 17 $\$
62	60, 61	sseqtr4i 3451	. . . . . . . . . . . . . . . 16 $\$
63		ssdif 3557	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
65		difundir 3687	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
66	64, 65	sseqtri 3450	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
67		difun1 3694	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
68		ssequn2 3598	. . . . . . . . . . . . . . . . . 18
69	47, 68	sylib 201	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
70	69	difeq2d 3540	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
71	67, 70	syl5eqr 2519	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
72	71	uneq1d 3578	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
73	66, 72	syl5sseq 3466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
74		ovolss 22516	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
75	73, 55, 74	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
76	37, 59, 46, 75, 57	letrd 9809	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
77	36, 37, 42, 46, 52, 76	le2addd 10253	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
78		simprl 772	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
79		mblsplit 22564	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
80	78, 40, 24, 79	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
81	80	oveq1d 6323	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
82	42	recnd 9687	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
83	45	recnd 9687	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
84	33	recnd 9687	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
85	82, 83, 84	addassd 9683	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
86	81, 85	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
87	77, 86	breqtrrd 4422	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
88		difss 3549	. . . . . . . . . . . 12 $\$
89		ovolss 22516	. . . . . . . . . . . 12 $\$ $/\$ $\$
90	88, 26, 89	sylancr 676	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
91	33, 31, 28, 90, 29	letrd 9809	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	33, 28, 24, 91	leadd2dd 10249	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93	23, 34, 35, 87, 92	letrd 9809	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
94	93	rexlimdvaa 2872	. . . . . . 7 $/\$ $/\$ $/\$ $\$
95	94	ralimdva 2805	. . . . . 6 $/\$ $/\$ $\$
96	95	impcom 437	. . . . 5 $/\$ $/\$ $/\$ $\$
97	22	adantl 473	. . . . . . 7 $/\$ $/\$ $/\$ $\$
98	97	rexrd 9708	. . . . . 6 $/\$ $/\$ $/\$ $\$
99		simprr 774	. . . . . 6 $/\$ $/\$ $/\$
100		xralrple 11521	. . . . . 6 $\$ $/\$ $\$ $\$
101	98, 99, 100	syl2anc 673	. . . . 5 $/\$ $/\$ $/\$ $\$ $\$
102	96, 101	mpbird 240	. . . 4 $/\$ $/\$ $/\$ $\$
103	102	expr 626	. . 3 $/\$ $/\$ $\$
104	103	ralrimiva 2809	. 2 $/\$ $\$
105		ismbl2 22559	. 2 $/\$ $\$
106	11, 104, 105	sylanbrc 677	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757 $\$ cdif 3387

cun 3388

cin 3389

wss 3390

c0 3722

cpw 3942 class class class wbr 4395

cdm 4839

cfv 5589 (class class class)co 6308

cr 9556

c1 9558

caddc 9560

cxr 9692

cle 9694

crp 11325

covol 22491

cvol 22493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-sup 7974 df-inf 7975 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-ioo 11664 df-ico 11666 df-icc 11667 df-fz 11811 df-fl 12061 df-seq 12252 df-exp 12311 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-ovol 22494 df-vol 22496

This theorem is referenced by: (None)

W3C validator