Metamath Proof Explorer

Theorem 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 ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ dom vol ( 𝐴 ⊆ 𝑦 ∧ ( vol* ‘ 𝑦 ) ≤ 𝑥 ) → 𝐴 ∈ dom vol )

Proof

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