Theorem uniiccmbl

Description: An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl .) (Contributed by Mario Carneiro, 25-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2		uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3		uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4	1	uniiccdif	⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) ∧ ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) = 0 ) )
5	4	simpld	⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) )
6		undif	⊢ ( ∪ ran ( (,) ∘ 𝐹 ) ⊆ ∪ ran ( [,] ∘ 𝐹 ) ↔ ( ∪ ran ( (,) ∘ 𝐹 ) ∪ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) = ∪ ran ( [,] ∘ 𝐹 ) )
7	5 6	sylib	⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐹 ) ∪ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) = ∪ ran ( [,] ∘ 𝐹 ) )
8	1 2 3	uniioombl	⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐹 ) ∈ dom vol )
9		ovolficcss	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
10	1 9	syl	⊢ ( 𝜑 → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
11	10	ssdifssd	⊢ ( 𝜑 → ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ⊆ ℝ )
12	4	simprd	⊢ ( 𝜑 → ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) = 0 )
13		nulmbl	⊢ ( ( ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ⊆ ℝ ∧ ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) = 0 ) → ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ dom vol )
14	11 12 13	syl2anc	⊢ ( 𝜑 → ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ dom vol )
15		unmbl	⊢ ( ( ∪ ran ( (,) ∘ 𝐹 ) ∈ dom vol ∧ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ∈ dom vol ) → ( ∪ ran ( (,) ∘ 𝐹 ) ∪ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ∈ dom vol )
16	8 14 15	syl2anc	⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐹 ) ∪ ( ∪ ran ( [,] ∘ 𝐹 ) ∖ ∪ ran ( (,) ∘ 𝐹 ) ) ) ∈ dom vol )
17	7 16	eqeltrrd	⊢ ( 𝜑 → ∪ ran ( [,] ∘ 𝐹 ) ∈ dom vol )