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 22490

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 11306	. . . . 5
2	1	ne0ii 3738	. . . 4
3		r19.2z 3858	. . . 4 $/\$ $/\$ $/\$
4	2, 3	mpan 676	. . 3 $/\$ $/\$
5		simprl 764	. . . . . 6 $/\$ $/\$
6		mblss 22485	. . . . . . 7
7	6	adantr 467	. . . . . 6 $/\$ $/\$
8	5, 7	sstrd 3442	. . . . 5 $/\$ $/\$
9	8	rexlimiva 2875	. . . 4 $/\$
10	9	rexlimivw 2876	. . 3 $/\$
11	4, 10	syl 17	. 2 $/\$
12		inss1 3652	. . . . . . . . . . . . 13
13	12	a1i 11	. . . . . . . . . . . 12 $/\$
14		elpwi 3960	. . . . . . . . . . . . 13
15	14	adantr 467	. . . . . . . . . . . 12 $/\$
16		simpr 463	. . . . . . . . . . . 12 $/\$
17		ovolsscl 22439	. . . . . . . . . . . 12 $/\$ $/\$
18	13, 15, 16, 17	syl3anc 1268	. . . . . . . . . . 11 $/\$
19		difssd 3561	. . . . . . . . . . . 12 $/\$ $\$
20		ovolsscl 22439	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$
21	19, 15, 16, 20	syl3anc 1268	. . . . . . . . . . 11 $/\$ $\$
22	18, 21	readdcld 9670	. . . . . . . . . 10 $/\$ $\$
23	22	ad2antrr 732	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
24	16	ad2antrr 732	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
25		difssd 3561	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
26	7	adantl 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
27		rpre 11308	. . . . . . . . . . . . 13
28	27	ad2antlr 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
29		simprrr 775	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
30		ovollecl 22436	. . . . . . . . . . . 12 $/\$ $/\$
31	26, 28, 29, 30	syl3anc 1268	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
32		ovolsscl 22439	. . . . . . . . . . 11 $\$ $/\$ $/\$ $\$
33	25, 26, 31, 32	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	24, 33	readdcld 9670	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
35	24, 28	readdcld 9670	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
36	18	ad2antrr 732	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
37	21	ad2antrr 732	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
38		inss1 3652	. . . . . . . . . . . . 13
39	38	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
40	15	ad2antrr 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
41		ovolsscl 22439	. . . . . . . . . . . 12 $/\$ $/\$
42	39, 40, 24, 41	syl3anc 1268	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
43		difssd 3561	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
44		ovolsscl 22439	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$
45	43, 40, 24, 44	syl3anc 1268	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46	45, 33	readdcld 9670	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
47		simprrl 774	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
48		sslin 3658	. . . . . . . . . . . . 13
49	47, 48	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
50	38, 40	syl5ss 3443	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
51		ovolss 22438	. . . . . . . . . . . 12 $/\$
52	49, 50, 51	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
53	40	ssdifssd 3571	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	26	ssdifssd 3571	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	53, 54	unssd 3610	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
56		ovolun 22452	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
57	53, 45, 54, 33, 56	syl22anc 1269	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
58		ovollecl 22436	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
59	55, 46, 57, 58	syl3anc 1268	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
60		ssun1 3597	. . . . . . . . . . . . . . . . 17
61		undif1 3842	. . . . . . . . . . . . . . . . 17 $\$
62	60, 61	sseqtr4i 3465	. . . . . . . . . . . . . . . 16 $\$
63		ssdif 3568	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
65		difundir 3696	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
66	64, 65	sseqtri 3464	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
67		difun1 3703	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
68		ssequn2 3607	. . . . . . . . . . . . . . . . . 18
69	47, 68	sylib 200	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
70	69	difeq2d 3551	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
71	67, 70	syl5eqr 2499	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
72	71	uneq1d 3587	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
73	66, 72	syl5sseq 3480	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
74		ovolss 22438	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
75	73, 55, 74	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
76	37, 59, 46, 75, 57	letrd 9792	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
77	36, 37, 42, 46, 52, 76	le2addd 10232	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
78		simprl 764	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
79		mblsplit 22486	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
80	78, 40, 24, 79	syl3anc 1268	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
81	80	oveq1d 6305	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
82	42	recnd 9669	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
83	45	recnd 9669	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
84	33	recnd 9669	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
85	82, 83, 84	addassd 9665	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
86	81, 85	eqtrd 2485	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
87	77, 86	breqtrrd 4429	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
88		difss 3560	. . . . . . . . . . . 12 $\$
89		ovolss 22438	. . . . . . . . . . . 12 $\$ $/\$ $\$
90	88, 26, 89	sylancr 669	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
91	33, 31, 28, 90, 29	letrd 9792	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	33, 28, 24, 91	leadd2dd 10228	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93	23, 34, 35, 87, 92	letrd 9792	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
94	93	rexlimdvaa 2880	. . . . . . 7 $/\$ $/\$ $/\$ $\$
95	94	ralimdva 2796	. . . . . 6 $/\$ $/\$ $\$
96	95	impcom 432	. . . . 5 $/\$ $/\$ $/\$ $\$
97	22	adantl 468	. . . . . . 7 $/\$ $/\$ $/\$ $\$
98	97	rexrd 9690	. . . . . 6 $/\$ $/\$ $/\$ $\$
99		simprr 766	. . . . . 6 $/\$ $/\$ $/\$
100		xralrple 11498	. . . . . 6 $\$ $/\$ $\$ $\$
101	98, 99, 100	syl2anc 667	. . . . 5 $/\$ $/\$ $/\$ $\$ $\$
102	96, 101	mpbird 236	. . . 4 $/\$ $/\$ $/\$ $\$
103	102	expr 620	. . 3 $/\$ $/\$ $\$
104	103	ralrimiva 2802	. 2 $/\$ $\$
105		ismbl2 22481	. 2 $/\$ $\$
106	11, 104, 105	sylanbrc 670	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371

wceq 1444

wcel 1887

wne 2622

wral 2737

wrex 2738 $\$ cdif 3401

cun 3402

cin 3403

wss 3404

c0 3731

cpw 3951 class class class wbr 4402

cdm 4834

cfv 5582 (class class class)co 6290

cr 9538

c1 9540

caddc 9542

cxr 9674

cle 9676

crp 11302

covol 22413

cvol 22415

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-er 7363 df-map 7474 df-en 7570 df-dom 7571 df-sdom 7572 df-sup 7956 df-inf 7957 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-q 11265 df-rp 11303 df-ioo 11639 df-ico 11641 df-icc 11642 df-fz 11785 df-fl 12028 df-seq 12214 df-exp 12273 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-ovol 22416 df-vol 22418

This theorem is referenced by: (None)

W3C validator