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 )