Theorem uniioombl 23873

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

Hypotheses

Ref	Expression
uniioombl.1	⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2	⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
uniioombl.3	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))

Assertion

Ref	Expression
uniioombl	⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol)

Distinct variable groups:   𝑥,𝐹   𝜑,𝑥

Allowed substitution hint:   𝑆(𝑥)

Proof of Theorem uniioombl

Dummy variables 𝑓 𝑟 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ioof 12685	. . . . 5 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2		uniioombl.1	. . . . . 6 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3		inss2 4128	. . . . . . 7 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
4		rexpssxrxp 10535	. . . . . . 7 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
5	3, 4	sstri 3900	. . . . . 6 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
6		fss 6398	. . . . . 6 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
7	2, 5, 6	sylancl 586	. . . . 5 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
8		fco 6402	. . . . 5 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
9	1, 7, 8	sylancr 587	. . . 4 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
10	9	frnd 6392	. . 3 ⊢ (𝜑 → ran ((,) ∘ 𝐹) ⊆ 𝒫 ℝ)
11		sspwuni 4923	. . 3 ⊢ (ran ((,) ∘ 𝐹) ⊆ 𝒫 ℝ ↔ ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
12	10, 11	sylib 219	. 2 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
13		elpwi 4465	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝒫 ℝ → 𝑧 ⊆ ℝ)
14	13	ad2antrl 724	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → 𝑧 ⊆ ℝ)
15		simprr 769	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → (vol*‘𝑧) ∈ ℝ)
16		rphalfcl 12266	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
17	16	rphalfcld 12293	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ+ → ((𝑟 / 2) / 2) ∈ ℝ+)
18		eqid 2794	. . . . . . . . . 10 ⊢ seq1( + , ((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − ) ∘ 𝑓))
19	18	ovolgelb 23764	. . . . . . . . 9 ⊢ ((𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ ∧ ((𝑟 / 2) / 2) ∈ ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))
20	14, 15, 17, 19	syl2an3an 1415	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))
21	2	ad3antrrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
22		uniioombl.2	. . . . . . . . . 10 ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
23	22	ad3antrrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
24		uniioombl.3	. . . . . . . . 9 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
25		eqid 2794	. . . . . . . . 9 ⊢ ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐹)
26	15	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → (vol*‘𝑧) ∈ ℝ)
27	26	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → (vol*‘𝑧) ∈ ℝ)
28	16	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈ ℝ+)
29	28	adantr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → (𝑟 / 2) ∈ ℝ+)
30	29	rphalfcld 12293	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → ((𝑟 / 2) / 2) ∈ ℝ+)
31		elmapi 8281	. . . . . . . . . 10 ⊢ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) → 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
32	31	ad2antrl 724	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝑓:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
33		simprrl 777	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → 𝑧 ⊆ ∪ ran ((,) ∘ 𝑓))
34		simprrr 778	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2)))
35	21, 23, 24, 25, 27, 30, 32, 33, 18, 34	uniioombllem6 23872	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) ∧ (𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ∧ (𝑧 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ≤ ((vol*‘𝑧) + ((𝑟 / 2) / 2))))) → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + (4 · ((𝑟 / 2) / 2))))
36	20, 35	rexlimddv 3253	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + (4 · ((𝑟 / 2) / 2))))
37		rpcn 12249	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℂ)
38	37	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℂ)
39		2cnd 11565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → 2 ∈ ℂ)
40		2ne0 11591	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
41	40	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → 2 ≠ 0)
42	38, 39, 39, 41, 41	divdiv1d 11297	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 / 2) / 2) = (𝑟 / (2 · 2)))
43		2t2e4 11651	. . . . . . . . . . . 12 ⊢ (2 · 2) = 4
44	43	oveq2i 7030	. . . . . . . . . . 11 ⊢ (𝑟 / (2 · 2)) = (𝑟 / 4)
45	42, 44	syl6eq 2846	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → ((𝑟 / 2) / 2) = (𝑟 / 4))
46	45	oveq2d 7035	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → (4 · ((𝑟 / 2) / 2)) = (4 · (𝑟 / 4)))
47		4cn 11572	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
48	47	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → 4 ∈ ℂ)
49		4ne0 11595	. . . . . . . . . . 11 ⊢ 4 ≠ 0
50	49	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → 4 ≠ 0)
51	38, 48, 50	divcan2d 11268	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → (4 · (𝑟 / 4)) = 𝑟)
52	46, 51	eqtrd 2830	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → (4 · ((𝑟 / 2) / 2)) = 𝑟)
53	52	oveq2d 7035	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → ((vol*‘𝑧) + (4 · ((𝑟 / 2) / 2))) = ((vol*‘𝑧) + 𝑟))
54	36, 53	breqtrd 4990	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) ∧ 𝑟 ∈ ℝ+) → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟))
55	54	ralrimiva 3148	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → ∀𝑟 ∈ ℝ+ ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟))
56		inss1 4127	. . . . . . . . 9 ⊢ (𝑧 ∩ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧
57	56	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → (𝑧 ∩ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧)
58		ovolsscl 23770	. . . . . . . 8 ⊢ (((𝑧 ∩ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) → (vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) ∈ ℝ)
59	57, 14, 15, 58	syl3anc 1364	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → (vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) ∈ ℝ)
60		difssd 4032	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → (𝑧 ∖ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧)
61		ovolsscl 23770	. . . . . . . 8 ⊢ (((𝑧 ∖ ∪ ran ((,) ∘ 𝐹)) ⊆ 𝑧 ∧ 𝑧 ⊆ ℝ ∧ (vol*‘𝑧) ∈ ℝ) → (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹))) ∈ ℝ)
62	60, 14, 15, 61	syl3anc 1364	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹))) ∈ ℝ)
63	59, 62	readdcld 10519	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ∈ ℝ)
64		alrple 12449	. . . . . 6 ⊢ ((((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ∈ ℝ ∧ (vol*‘𝑧) ∈ ℝ) → (((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧) ↔ ∀𝑟 ∈ ℝ+ ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟)))
65	63, 15, 64	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → (((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧) ↔ ∀𝑟 ∈ ℝ+ ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ ((vol*‘𝑧) + 𝑟)))
66	55, 65	mpbird 258	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝒫 ℝ ∧ (vol*‘𝑧) ∈ ℝ)) → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧))
67	66	expr 457	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 ℝ) → ((vol*‘𝑧) ∈ ℝ → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧)))
68	67	ralrimiva 3148	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 ℝ((vol*‘𝑧) ∈ ℝ → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧)))
69		ismbl2 23811	. 2 ⊢ (∪ ran ((,) ∘ 𝐹) ∈ dom vol ↔ (∪ ran ((,) ∘ 𝐹) ⊆ ℝ ∧ ∀𝑧 ∈ 𝒫 ℝ((vol*‘𝑧) ∈ ℝ → ((vol*‘(𝑧 ∩ ∪ ran ((,) ∘ 𝐹))) + (vol*‘(𝑧 ∖ ∪ ran ((,) ∘ 𝐹)))) ≤ (vol*‘𝑧))))
70	12, 68, 69	sylanbrc 583	1 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2080   ≠ wne 2983  ∀wral 3104  ∃wrex 3105   ∖ cdif 3858   ∩ cin 3860   ⊆ wss 3861  𝒫 cpw 4455  ∪ cuni 4747  Disj wdisj 4932   class class class wbr 4964   × cxp 5444  dom cdm 5446  ran crn 5447   ∘ ccom 5450  ⟶wf 6224  ‘cfv 6228  (class class class)co 7019   ↑_𝑚 cmap 8259  supcsup 8753  ℂcc 10384  ℝcr 10385  0cc0 10386  1c1 10387   + caddc 10389   · cmul 10391  ℝ^*cxr 10523   < clt 10524   ≤ cle 10525   − cmin 10719   / cdiv 11147  ℕcn 11488  2c2 11542  4c4 11544  ℝ⁺crp 12239  (,)cioo 12588  seqcseq 13219  abscabs 14427  vol*covol 23746  volcvol 23747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-inf2 8953  ax-cnex 10442  ax-resscn 10443  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-addrcl 10447  ax-mulcl 10448  ax-mulrcl 10449  ax-mulcom 10450  ax-addass 10451  ax-mulass 10452  ax-distr 10453  ax-i2m1 10454  ax-1ne0 10455  ax-1rid 10456  ax-rnegex 10457  ax-rrecex 10458  ax-cnre 10459  ax-pre-lttri 10460  ax-pre-lttrn 10461  ax-pre-ltadd 10462  ax-pre-mulgt0 10463  ax-pre-sup 10464

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-nel 3090  df-ral 3109  df-rex 3110  df-reu 3111  df-rmo 3112  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-int 4785  df-iun 4829  df-disj 4933  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-se 5406  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-isom 6237  df-riota 6980  df-ov 7022  df-oprab 7023  df-mpo 7024  df-of 7270  df-om 7440  df-1st 7548  df-2nd 7549  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-2o 7957  df-oadd 7960  df-er 8142  df-map 8261  df-pm 8262  df-en 8361  df-dom 8362  df-sdom 8363  df-fin 8364  df-fi 8724  df-sup 8755  df-inf 8756  df-oi 8823  df-dju 9179  df-card 9217  df-acn 9220  df-pnf 10526  df-mnf 10527  df-xr 10528  df-ltxr 10529  df-le 10530  df-sub 10721  df-neg 10722  df-div 11148  df-nn 11489  df-2 11550  df-3 11551  df-4 11552  df-n0 11748  df-z 11832  df-uz 12094  df-q 12198  df-rp 12240  df-xneg 12357  df-xadd 12358  df-xmul 12359  df-ioo 12592  df-ico 12594  df-icc 12595  df-fz 12743  df-fzo 12884  df-fl 13012  df-seq 13220  df-exp 13280  df-hash 13541  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-clim 14679  df-rlim 14680  df-sum 14877  df-rest 16525  df-topgen 16546  df-psmet 20219  df-xmet 20220  df-met 20221  df-bl 20222  df-mopn 20223  df-top 21186  df-topon 21203  df-bases 21238  df-cmp 21679  df-ovol 23748  df-vol 23749

This theorem is referenced by:  uniiccmbl  23874