nulmbl2 - Metamath Proof Explorer

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

Theorem nulmbl2 22073

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 11249	. . . . 5
2	1	ne0ii 3800	. . . 4
3		r19.2z 3921	. . . 4 $/\$ $/\$ $/\$
4	2, 3	mpan 670	. . 3 $/\$ $/\$
5		simprl 756	. . . . . 6 $/\$ $/\$
6		mblss 22068	. . . . . . 7
7	6	adantr 465	. . . . . 6 $/\$ $/\$
8	5, 7	sstrd 3509	. . . . 5 $/\$ $/\$
9	8	rexlimiva 2945	. . . 4 $/\$
10	9	rexlimivw 2946	. . 3 $/\$
11	4, 10	syl 16	. 2 $/\$
12		inss1 3714	. . . . . . . . . . . . 13
13	12	a1i 11	. . . . . . . . . . . 12 $/\$
14		elpwi 4024	. . . . . . . . . . . . 13
15	14	adantr 465	. . . . . . . . . . . 12 $/\$
16		simpr 461	. . . . . . . . . . . 12 $/\$
17		ovolsscl 22023	. . . . . . . . . . . 12 $/\$ $/\$
18	13, 15, 16, 17	syl3anc 1228	. . . . . . . . . . 11 $/\$
19		difssd 3628	. . . . . . . . . . . 12 $/\$ $\$
20		ovolsscl 22023	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$
21	19, 15, 16, 20	syl3anc 1228	. . . . . . . . . . 11 $/\$ $\$
22	18, 21	readdcld 9640	. . . . . . . . . 10 $/\$ $\$
23	22	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
24	16	ad2antrr 725	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
25		difssd 3628	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
26	7	adantl 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
27		rpre 11251	. . . . . . . . . . . . 13
28	27	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
29		simprrr 766	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
30		ovollecl 22020	. . . . . . . . . . . 12 $/\$ $/\$
31	26, 28, 29, 30	syl3anc 1228	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
32		ovolsscl 22023	. . . . . . . . . . 11 $\$ $/\$ $/\$ $\$
33	25, 26, 31, 32	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	24, 33	readdcld 9640	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
35	24, 28	readdcld 9640	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
36	18	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
37	21	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
38		inss1 3714	. . . . . . . . . . . . 13
39	38	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
40	15	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
41		ovolsscl 22023	. . . . . . . . . . . 12 $/\$ $/\$
42	39, 40, 24, 41	syl3anc 1228	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
43		difssd 3628	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
44		ovolsscl 22023	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$
45	43, 40, 24, 44	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46	45, 33	readdcld 9640	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
47		simprrl 765	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
48		sslin 3720	. . . . . . . . . . . . 13
49	47, 48	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
50	38, 40	syl5ss 3510	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
51		ovolss 22022	. . . . . . . . . . . 12 $/\$
52	49, 50, 51	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
53	40	ssdifssd 3638	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
54	26	ssdifssd 3638	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
55	53, 54	unssd 3676	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
56		ovolun 22036	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
57	53, 45, 54, 33, 56	syl22anc 1229	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
58		ovollecl 22020	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
59	55, 46, 57, 58	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
60		ssun1 3663	. . . . . . . . . . . . . . . . 17
61		undif1 3906	. . . . . . . . . . . . . . . . 17 $\$
62	60, 61	sseqtr4i 3532	. . . . . . . . . . . . . . . 16 $\$
63		ssdif 3635	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
65		difundir 3758	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$ $\$
66	64, 65	sseqtri 3531	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
67		difun1 3765	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
68		ssequn2 3673	. . . . . . . . . . . . . . . . . 18
69	47, 68	sylib 196	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
70	69	difeq2d 3618	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
71	67, 70	syl5eqr 2512	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
72	71	uneq1d 3653	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$ $\$
73	66, 72	syl5sseq 3547	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
74		ovolss 22022	. . . . . . . . . . . . 13 $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
75	73, 55, 74	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
76	37, 59, 46, 75, 57	letrd 9756	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
77	36, 37, 42, 46, 52, 76	le2addd 10191	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
78		simprl 756	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
79		mblsplit 22069	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
80	78, 40, 24, 79	syl3anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
81	80	oveq1d 6311	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
82	42	recnd 9639	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
83	45	recnd 9639	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
84	33	recnd 9639	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
85	82, 83, 84	addassd 9635	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
86	81, 85	eqtrd 2498	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
87	77, 86	breqtrrd 4482	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
88		difss 3627	. . . . . . . . . . . 12 $\$
89		ovolss 22022	. . . . . . . . . . . 12 $\$ $/\$ $\$
90	88, 26, 89	sylancr 663	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
91	33, 31, 28, 90, 29	letrd 9756	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	33, 28, 24, 91	leadd2dd 10188	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93	23, 34, 35, 87, 92	letrd 9756	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
94	93	rexlimdvaa 2950	. . . . . . 7 $/\$ $/\$ $/\$ $\$
95	94	ralimdva 2865	. . . . . 6 $/\$ $/\$ $\$
96	95	impcom 430	. . . . 5 $/\$ $/\$ $/\$ $\$
97	22	adantl 466	. . . . . . 7 $/\$ $/\$ $/\$ $\$
98	97	rexrd 9660	. . . . . 6 $/\$ $/\$ $/\$ $\$
99		simprr 757	. . . . . 6 $/\$ $/\$ $/\$
100		xralrple 11429	. . . . . 6 $\$ $/\$ $\$ $\$
101	98, 99, 100	syl2anc 661	. . . . 5 $/\$ $/\$ $/\$ $\$ $\$
102	96, 101	mpbird 232	. . . 4 $/\$ $/\$ $/\$ $\$
103	102	expr 615	. . 3 $/\$ $/\$ $\$
104	103	ralrimiva 2871	. 2 $/\$ $\$
105		ismbl2 22064	. 2 $/\$ $\$
106	11, 104, 105	sylanbrc 664	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1395

wcel 1819

wne 2652

wral 2807

wrex 2808 $\$ cdif 3468

cun 3469

cin 3470

wss 3471

c0 3793

cpw 4015 class class class wbr 4456

cdm 5008

cfv 5594 (class class class)co 6296

cr 9508

c1 9510

caddc 9512

cxr 9644

cle 9646

crp 11245

covol 22000

cvol 22001

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-er 7329 df-map 7440 df-en 7536 df-dom 7537 df-sdom 7538 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-ioo 11558 df-ico 11560 df-icc 11561 df-fz 11698 df-fl 11932 df-seq 12111 df-exp 12170 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-ovol 22002 df-vol 22003

This theorem is referenced by: (None)

W3C validator