This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniioombl

Description: A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl .) Lemma 565Ca of Fremlin5 p. 214. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
Assertion uniioombl ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3 uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
5 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
6 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
7 5 6 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
8 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
9 1 7 8 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
10 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
11 4 9 10 sylancr ⊢ ( 𝜑 → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
12 11 frnd ⊢ ( 𝜑 → ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ )
13 sspwuni ⊢ ( ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ ↔ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
14 12 13 sylib ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
15 elpwi ⊢ ( 𝑧 ∈ 𝒫 ℝ → 𝑧 ⊆ ℝ )
16 15 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → 𝑧 ⊆ ℝ )
17 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( vol* ‘ 𝑧 ) ∈ ℝ )
18 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
19 18 rphalfcld ⊢ ( 𝑟 ∈ ℝ+ → ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ )
20 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
21 20 ovolgelb ⊢ ( ( 𝑧 ⊆ ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ∧ ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) )
22 16 17 19 21 syl2an3an ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) )
23 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
24 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
25 eqid ⊢ ∪ ran ( (,) ∘ 𝐹 ) = ∪ ran ( (,) ∘ 𝐹 )
26 17 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( vol* ‘ 𝑧 ) ∈ ℝ )
27 26 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → ( vol* ‘ 𝑧 ) ∈ ℝ )
28 18 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ+ )
29 28 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
30 29 rphalfcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ )
31 elmapi ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
32 31 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
33 simprrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) )
34 simprrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) )
35 23 24 3 25 27 30 32 33 20 34 uniioombllem6 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝑧 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝑧 ) + ( ( 𝑟 / 2 ) / 2 ) ) ) ) ) → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( ( vol* ‘ 𝑧 ) + ( 4 · ( ( 𝑟 / 2 ) / 2 ) ) ) )
36 22 35 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( ( vol* ‘ 𝑧 ) + ( 4 · ( ( 𝑟 / 2 ) / 2 ) ) ) )
37 rpcn ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℂ )
38 37 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℂ )
39 2cnd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → 2 ∈ ℂ )
40 2ne0 ⊢ 2 ≠ 0
41 40 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → 2 ≠ 0 )
42 38 39 39 41 41 divdiv1d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑟 / 2 ) / 2 ) = ( 𝑟 / ( 2 · 2 ) ) )
43 2t2e4 ⊢ ( 2 · 2 ) = 4
44 43 oveq2i ⊢ ( 𝑟 / ( 2 · 2 ) ) = ( 𝑟 / 4 )
45 42 44 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑟 / 2 ) / 2 ) = ( 𝑟 / 4 ) )
46 45 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 4 · ( ( 𝑟 / 2 ) / 2 ) ) = ( 4 · ( 𝑟 / 4 ) ) )
47 4cn ⊢ 4 ∈ ℂ
48 47 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → 4 ∈ ℂ )
49 4ne0 ⊢ 4 ≠ 0
50 49 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → 4 ≠ 0 )
51 38 48 50 divcan2d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 4 · ( 𝑟 / 4 ) ) = 𝑟 )
52 46 51 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 4 · ( ( 𝑟 / 2 ) / 2 ) ) = 𝑟 )
53 52 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( vol* ‘ 𝑧 ) + ( 4 · ( ( 𝑟 / 2 ) / 2 ) ) ) = ( ( vol* ‘ 𝑧 ) + 𝑟 ) )
54 36 53 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( ( vol* ‘ 𝑧 ) + 𝑟 ) )
55 54 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ∀ 𝑟 ∈ ℝ+ ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( ( vol* ‘ 𝑧 ) + 𝑟 ) )
56 inss1 ⊢ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ⊆ 𝑧
57 56 a1i ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ⊆ 𝑧 )
58 ovolsscl ⊢ ( ( ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) → ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) ∈ ℝ )
59 57 16 17 58 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) ∈ ℝ )
60 difssd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ⊆ 𝑧 )
61 ovolsscl ⊢ ( ( ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) → ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ∈ ℝ )
62 60 16 17 61 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ∈ ℝ )
63 59 62 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ∈ ℝ )
64 alrple ⊢ ( ( ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ∈ ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) → ( ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( vol* ‘ 𝑧 ) ↔ ∀ 𝑟 ∈ ℝ+ ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( ( vol* ‘ 𝑧 ) + 𝑟 ) ) )
65 63 17 64 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( vol* ‘ 𝑧 ) ↔ ∀ 𝑟 ∈ ℝ+ ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( ( vol* ‘ 𝑧 ) + 𝑟 ) ) )
66 55 65 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑧 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( vol* ‘ 𝑧 ) )
67 66 expr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 ℝ ) → ( ( vol* ‘ 𝑧 ) ∈ ℝ → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( vol* ‘ 𝑧 ) ) )
68 67 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑧 ) ∈ ℝ → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( vol* ‘ 𝑧 ) ) )
69 ismbl2 ⊢ ( ∪ ran ( (,) ∘ 𝐹 ) ∈ dom vol ↔ ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑧 ) ∈ ℝ → ( ( vol* ‘ ( 𝑧 ∩ ∪ ran ( (,) ∘ 𝐹 ) ) ) + ( vol* ‘ ( 𝑧 ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ) ≤ ( vol* ‘ 𝑧 ) ) ) )
70 14 68 69 sylanbrc ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ∈ dom vol )