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

Metamath Proof Explorer

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 )