nulmbl2

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 vol* ( A ) = 0 while "outer measure zero" means that for any x there is a y containing A with volume less than x . Assuming AC, these notions are equivalent (because the intersection of all such y 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)

		Ref	Expression
	Assertion	nulmbl2	$⊢ \forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{*} (y) \leq x) \to A \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		1rp	$⊢ 1 \in ℝ^{+}$
2	1	ne0ii	$⊢ ℝ^{+} \neq \emptyset$
3		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x)) \to \exists x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x)$
4	2 3	mpan	$⊢ \forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \to \exists x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x)$
5		simprl	$⊢ (y \in dom vol \land (A \subseteq y \land {vol}^{*} (y) \leq x)) \to A \subseteq y$
6		mblss	$⊢ y \in dom vol \to y \subseteq ℝ$
7	6	adantr	$⊢ (y \in dom vol \land (A \subseteq y \land {vol}^{*} (y) \leq x)) \to y \subseteq ℝ$
8	5 7	sstrd	$⊢ (y \in dom vol \land (A \subseteq y \land {vol}^{*} (y) \leq x)) \to A \subseteq ℝ$
9	8	rexlimiva	$⊢ \exists y \in dom vol (A \subseteq y \land {vol}^{*} (y) \leq x) \to A \subseteq ℝ$
10	9	rexlimivw	$⊢ \exists x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{*} (y) \leq x) \to A \subseteq ℝ$
11	4 10	syl	$⊢ \forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{*} (y) \leq x) \to A \subseteq ℝ$
12		inss1	$⊢ z \cap A \subseteq z$
13		elpwi	$⊢ z \in 𝒫 ℝ \to z \subseteq ℝ$
14	13	adantr	$⊢ (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ) \to z \subseteq ℝ$
15		simpr	$⊢ (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z) \in ℝ$
16		ovolsscl	$⊢ (z \cap A \subseteq z \land z \subseteq ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z \cap A) \in ℝ$
17	12 14 15 16	mp3an2i	$⊢ (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z \cap A) \in ℝ$
18		difssd	$⊢ (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ) \to z ∖ A \subseteq z$
19		ovolsscl	$⊢ (z ∖ A \subseteq z \land z \subseteq ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z ∖ A) \in ℝ$
20	18 14 15 19	syl3anc	$⊢ (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z ∖ A) \in ℝ$
21	17 20	readdcld	$⊢ (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z \cap A) + {vol}^{*} (z ∖ A) \in ℝ$
22	21	ad2antrr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \in ℝ$
23	15	ad2antrr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z) \in ℝ$
24		difssd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to y ∖ A \subseteq y$
25	7	adantl	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to y \subseteq ℝ$
26		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
27	26	ad2antlr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to x \in ℝ$
28		simprrr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (y) \leq x$
29		ovollecl	$⊢ (y \subseteq ℝ \land x \in ℝ \land {vol}^{} (y) \leq x) \to {vol}^{} (y) \in ℝ$
30	25 27 28 29	syl3anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (y) \in ℝ$
31		ovolsscl	$⊢ (y ∖ A \subseteq y \land y \subseteq ℝ \land {vol}^{} (y) \in ℝ) \to {vol}^{} (y ∖ A) \in ℝ$
32	24 25 30 31	syl3anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (y ∖ A) \in ℝ$
33	23 32	readdcld	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z) + {vol}^{} (y ∖ A) \in ℝ$
34	23 27	readdcld	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z) + x \in ℝ$
35	17	ad2antrr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z \cap A) \in ℝ$
36	20	ad2antrr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z ∖ A) \in ℝ$
37		inss1	$⊢ z \cap y \subseteq z$
38	14	ad2antrr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to z \subseteq ℝ$
39		ovolsscl	$⊢ (z \cap y \subseteq z \land z \subseteq ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z \cap y) \in ℝ$
40	37 38 23 39	mp3an2i	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z \cap y) \in ℝ$
41		difssd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to z ∖ y \subseteq z$
42		ovolsscl	$⊢ (z ∖ y \subseteq z \land z \subseteq ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z ∖ y) \in ℝ$
43	41 38 23 42	syl3anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z ∖ y) \in ℝ$
44	43 32	readdcld	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z ∖ y) + {vol}^{} (y ∖ A) \in ℝ$
45		simprrl	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to A \subseteq y$
46		sslin	$⊢ A \subseteq y \to z \cap A \subseteq z \cap y$
47	45 46	syl	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to z \cap A \subseteq z \cap y$
48	37 38	sstrid	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to z \cap y \subseteq ℝ$
49		ovolss	$⊢ (z \cap A \subseteq z \cap y \land z \cap y \subseteq ℝ) \to {vol}^{} (z \cap A) \leq {vol}^{} (z \cap y)$
50	47 48 49	syl2anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z \cap A) \leq {vol}^{} (z \cap y)$
51	38	ssdifssd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to z ∖ y \subseteq ℝ$
52	25	ssdifssd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to y ∖ A \subseteq ℝ$
53	51 52	unssd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to (z ∖ y) \cup (y ∖ A) \subseteq ℝ$
54		ovolun	$⊢ ((z ∖ y \subseteq ℝ \land {vol}^{} (z ∖ y) \in ℝ) \land (y ∖ A \subseteq ℝ \land {vol}^{} (y ∖ A) \in ℝ)) \to {vol}^{} ((z ∖ y) \cup (y ∖ A)) \leq {vol}^{} (z ∖ y) + {vol}^{*} (y ∖ A)$
55	51 43 52 32 54	syl22anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} ((z ∖ y) \cup (y ∖ A)) \leq {vol}^{} (z ∖ y) + {vol}^{*} (y ∖ A)$
56		ovollecl	$⊢ ((z ∖ y) \cup (y ∖ A) \subseteq ℝ \land {vol}^{} (z ∖ y) + {vol}^{} (y ∖ A) \in ℝ \land {vol}^{} ((z ∖ y) \cup (y ∖ A)) \leq {vol}^{} (z ∖ y) + {vol}^{} (y ∖ A)) \to {vol}^{} ((z ∖ y) \cup (y ∖ A)) \in ℝ$
57	53 44 55 56	syl3anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} ((z ∖ y) \cup (y ∖ A)) \in ℝ$
58		ssun1	$⊢ z \subseteq z \cup y$
59		undif1	$⊢ (z ∖ y) \cup y = z \cup y$
60	58 59	sseqtrri	$⊢ z \subseteq (z ∖ y) \cup y$
61		ssdif	$⊢ z \subseteq (z ∖ y) \cup y \to z ∖ A \subseteq ((z ∖ y) \cup y) ∖ A$
62	60 61	ax-mp	$⊢ z ∖ A \subseteq ((z ∖ y) \cup y) ∖ A$
63		difundir	$⊢ ((z ∖ y) \cup y) ∖ A = ((z ∖ y) ∖ A) \cup (y ∖ A)$
64	62 63	sseqtri	$⊢ z ∖ A \subseteq ((z ∖ y) ∖ A) \cup (y ∖ A)$
65		difun1	$⊢ z ∖ (y \cup A) = (z ∖ y) ∖ A$
66		ssequn2	$⊢ A \subseteq y \leftrightarrow y \cup A = y$
67	45 66	sylib	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to y \cup A = y$
68	67	difeq2d	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to z ∖ (y \cup A) = z ∖ y$
69	65 68	eqtr3id	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to (z ∖ y) ∖ A = z ∖ y$
70	69	uneq1d	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to ((z ∖ y) ∖ A) \cup (y ∖ A) = (z ∖ y) \cup (y ∖ A)$
71	64 70	sseqtrid	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to z ∖ A \subseteq (z ∖ y) \cup (y ∖ A)$
72		ovolss	$⊢ (z ∖ A \subseteq (z ∖ y) \cup (y ∖ A) \land (z ∖ y) \cup (y ∖ A) \subseteq ℝ) \to {vol}^{} (z ∖ A) \leq {vol}^{} ((z ∖ y) \cup (y ∖ A))$
73	71 53 72	syl2anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z ∖ A) \leq {vol}^{} ((z ∖ y) \cup (y ∖ A))$
74	36 57 44 73 55	letrd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z ∖ A) \leq {vol}^{} (z ∖ y) + {vol}^{*} (y ∖ A)$
75	35 36 40 44 50 74	le2addd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{} (z \cap y) + {vol}^{} (z ∖ y) + {vol}^{*} (y ∖ A)$
76		simprl	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to y \in dom vol$
77		mblsplit	$⊢ (y \in dom vol \land z \subseteq ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z) = {vol}^{} (z \cap y) + {vol}^{} (z ∖ y)$
78	76 38 23 77	syl3anc	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z) = {vol}^{} (z \cap y) + {vol}^{*} (z ∖ y)$
79	78	oveq1d	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z) + {vol}^{} (y ∖ A) = {vol}^{} (z \cap y) + {vol}^{} (z ∖ y) + {vol}^{*} (y ∖ A)$
80	40	recnd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z \cap y) \in ℂ$
81	43	recnd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (z ∖ y) \in ℂ$
82	32	recnd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (y ∖ A) \in ℂ$
83	80 81 82	addassd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z \cap y) + {vol}^{} (z ∖ y) + {vol}^{} (y ∖ A) = {vol}^{} (z \cap y) + {vol}^{} (z ∖ y) + {vol}^{} (y ∖ A)$
84	79 83	eqtrd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z) + {vol}^{} (y ∖ A) = {vol}^{} (z \cap y) + {vol}^{} (z ∖ y) + {vol}^{*} (y ∖ A)$
85	75 84	breqtrrd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{} (z) + {vol}^{} (y ∖ A)$
86		difss	$⊢ y ∖ A \subseteq y$
87		ovolss	$⊢ (y ∖ A \subseteq y \land y \subseteq ℝ) \to {vol}^{} (y ∖ A) \leq {vol}^{} (y)$
88	86 25 87	sylancr	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (y ∖ A) \leq {vol}^{} (y)$
89	32 30 27 88 28	letrd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{*} (y ∖ A) \leq x$
90	32 27 23 89	leadd2dd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z) + {vol}^{} (y ∖ A) \leq {vol}^{*} (z) + x$
91	22 33 34 85 90	letrd	$⊢ (((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \land (y \in dom vol \land (A \subseteq y \land {vol}^{} (y) \leq x))) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{*} (z) + x$
92	91	rexlimdvaa	$⊢ ((z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \land x \in ℝ^{+}) \to (\exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{*} (z) + x)$
93	92	ralimdva	$⊢ (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ) \to (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \to \forall x \in ℝ^{+} {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{*} (z) + x)$
94	93	impcom	$⊢ (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to \forall x \in ℝ^{+} {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{*} (z) + x$
95	21	adantl	$⊢ (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \in ℝ$
96	95	rexrd	$⊢ (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \in ℝ^{*}$
97		simprr	$⊢ (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{*} (z) \in ℝ$
98		xralrple	$⊢ ({vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \in ℝ^{} \land {vol}^{} (z) \in ℝ) \to ({vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{} (z) \leftrightarrow \forall x \in ℝ^{+} {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{} (z) + x)$
99	96 97 98	syl2anc	$⊢ (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to ({vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{} (z) \leftrightarrow \forall x \in ℝ^{+} {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{} (z) + x)$
100	94 99	mpbird	$⊢ (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{*} (z)$
101	100	expr	$⊢ (\forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \land z \in 𝒫 ℝ) \to ({vol}^{} (z) \in ℝ \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{*} (z))$
102	101	ralrimiva	$⊢ \forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{} (y) \leq x) \to \forall z \in 𝒫 ℝ ({vol}^{} (z) \in ℝ \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{*} (z))$
103		ismbl2	$⊢ A \in dom vol \leftrightarrow (A \subseteq ℝ \land \forall z \in 𝒫 ℝ ({vol}^{} (z) \in ℝ \to {vol}^{} (z \cap A) + {vol}^{} (z ∖ A) \leq {vol}^{} (z)))$
104	11 102 103	sylanbrc	$⊢ \forall x \in ℝ^{+} \exists y \in dom vol (A \subseteq y \land {vol}^{*} (y) \leq x) \to A \in dom vol$

Metamath Proof Explorer

Theorem nulmbl2

Proof