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 )

Metamath Proof Explorer

Theorem uniioombl

Proof