nulmbl2 - Metamath Proof Explorer

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

Theorem nulmbl2 21774

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 11225	. . . . 5
2		ne0i 3791	. . . . 5
3	1, 2	ax-mp 5	. . . 4
4		r19.2z 3917	. . . 4 $/\$ $/\$ $/\$
5	3, 4	mpan 670	. . 3 $/\$ $/\$
6		simprl 755	. . . . . 6 $/\$ $/\$
7		mblss 21769	. . . . . . 7
8	7	adantr 465	. . . . . 6 $/\$ $/\$
9	6, 8	sstrd 3514	. . . . 5 $/\$ $/\$
10	9	rexlimiva 2951	. . . 4 $/\$
11	10	rexlimivw 2952	. . 3 $/\$
12	5, 11	syl 16	. 2 $/\$
13		inss1 3718	. . . . . . . . . . . . 13
14	13	a1i 11	. . . . . . . . . . . 12 $/\$
15		elpwi 4019	. . . . . . . . . . . . 13
16	15	adantr 465	. . . . . . . . . . . 12 $/\$
17		simpr 461	. . . . . . . . . . . 12 $/\$
18		ovolsscl 21724	. . . . . . . . . . . 12 $/\$ $/\$
19	14, 16, 17, 18	syl3anc 1228	. . . . . . . . . . 11 $/\$
20		difssd 3632	. . . . . . . . . . . 12 $/\$ $\$
21		ovolsscl 21724	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$
22	20, 16, 17, 21	syl3anc 1228	. . . . . . . . . . 11 $/\$ $\$
23	19, 22	readdcld 9624	. . . . . . . . . 10 $/\$ $\$
24	23	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
25	17	ad2antrr 725	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26		difssd 3632	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
27	8	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
28		rpre 11227	. . . . . . . . . . . . 13
29	28	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
30		simprrr 764	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
31		ovollecl 21721	. . . . . . . . . . . 12 $/\$ $/\$
32	27, 29, 30, 31	syl3anc 1228	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33		ovolsscl 21724	. . . . . . . . . . 11 $\$ $/\$ $/\$ $\$
34	26, 27, 32, 33	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
35	25, 34	readdcld 9624	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
36	25, 29	readdcld 9624	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
37	19	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
38	22	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
39		inss1 3718	. . . . . . . . . . . . 13
40	39	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
41	16	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
42		ovolsscl 21724	. . . . . . . . . . . 12 $/\$ $/\$
43	40, 41, 25, 42	syl3anc 1228	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
44		difssd 3632	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
45		ovolsscl 21724	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$
46	44, 41, 25, 45	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
47	46, 34	readdcld 9624	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
48		simprrl 763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
49		sslin 3724	. . . . . . . . . . . . 13
50	48, 49	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
51	39, 41	syl5ss 3515	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
52		ovolss 21723	. . . . . . . . . . . 12 $/\$
53	50, 51, 52	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
54	41	ssdifssd 3642	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	27	ssdifssd 3642	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
56	54, 55	unssd 3680	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
57		ovolun 21737	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
58	54, 46, 55, 34, 57	syl22anc 1229	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
59		ovollecl 21721	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
60	56, 47, 58, 59	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
61		ssun1 3667	. . . . . . . . . . . . . . . . 17
62		undif1 3902	. . . . . . . . . . . . . . . . 17 $\$
63	61, 62	sseqtr4i 3537	. . . . . . . . . . . . . . . 16 $\$
64		ssdif 3639	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
65	63, 64	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
66		difundir 3751	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
67	65, 66	sseqtri 3536	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
68		difun1 3758	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
69		ssequn2 3677	. . . . . . . . . . . . . . . . . 18
70	48, 69	sylib 196	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	difeq2d 3622	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
72	68, 71	syl5eqr 2522	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
73	72	uneq1d 3657	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
74	67, 73	syl5sseq 3552	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
75		ovolss 21723	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
76	74, 56, 75	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
77	38, 60, 47, 76, 58	letrd 9739	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
78	37, 38, 43, 47, 53, 77	le2addd 10171	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
79		simprl 755	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
80		mblsplit 21770	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
81	79, 41, 25, 80	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
82	81	oveq1d 6300	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
83	43	recnd 9623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
84	46	recnd 9623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
85	34	recnd 9623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
86	83, 84, 85	addassd 9619	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
87	82, 86	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
88	78, 87	breqtrrd 4473	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
89		difss 3631	. . . . . . . . . . . 12 $\$
90		ovolss 21723	. . . . . . . . . . . 12 $\$ $/\$ $\$
91	89, 27, 90	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	34, 32, 29, 91, 30	letrd 9739	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93	34, 29, 25, 92	leadd2dd 10168	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
94	24, 35, 36, 88, 93	letrd 9739	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
95	94	rexlimdvaa 2956	. . . . . . 7 $/\$ $/\$ $/\$ $\$
96	95	ralimdva 2872	. . . . . 6 $/\$ $/\$ $\$
97	96	impcom 430	. . . . 5 $/\$ $/\$ $/\$ $\$
98	23	adantl 466	. . . . . . 7 $/\$ $/\$ $/\$ $\$
99	98	rexrd 9644	. . . . . 6 $/\$ $/\$ $/\$ $\$
100		simprr 756	. . . . . 6 $/\$ $/\$ $/\$
101		xralrple 11405	. . . . . 6 $\$ $/\$ $\$ $\$
102	99, 100, 101	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $\$ $\$
103	97, 102	mpbird 232	. . . 4 $/\$ $/\$ $/\$ $\$
104	103	expr 615	. . 3 $/\$ $/\$ $\$
105	104	ralrimiva 2878	. 2 $/\$ $\$
106		ismbl2 21765	. 2 $/\$ $\$
107	12, 105, 106	sylanbrc 664	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662

wral 2814

wrex 2815 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

cpw 4010 class class class wbr 4447

cdm 4999

cfv 5588 (class class class)co 6285

cr 9492

c1 9494

caddc 9496

cxr 9628

cle 9630

crp 11221

covol 21701

cvol 21702

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6577 ax-cnex 9549 ax-resscn 9550 ax-1cn 9551 ax-icn 9552 ax-addcl 9553 ax-addrcl 9554 ax-mulcl 9555 ax-mulrcl 9556 ax-mulcom 9557 ax-addass 9558 ax-mulass 9559 ax-distr 9560 ax-i2m1 9561 ax-1ne0 9562 ax-1rid 9563 ax-rnegex 9564 ax-rrecex 9565 ax-cnre 9566 ax-pre-lttri 9567 ax-pre-lttrn 9568 ax-pre-ltadd 9569 ax-pre-mulgt0 9570 ax-pre-sup 9571

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6246 df-ov 6288 df-oprab 6289 df-mpt2 6290 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7043 df-rdg 7077 df-er 7312 df-map 7423 df-en 7518 df-dom 7519 df-sdom 7520 df-sup 7902 df-pnf 9631 df-mnf 9632 df-xr 9633 df-ltxr 9634 df-le 9635 df-sub 9808 df-neg 9809 df-div 10208 df-nn 10538 df-2 10595 df-3 10596 df-n0 10797 df-z 10866 df-uz 11084 df-q 11184 df-rp 11222 df-ioo 11534 df-ico 11536 df-icc 11537 df-fz 11674 df-fl 11898 df-seq 12077 df-exp 12136 df-cj 12898 df-re 12899 df-im 12900 df-sqrt 13034 df-abs 13035 df-ovol 21703 df-vol 21704

This theorem is referenced by: (None)

W3C validator