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

Metamath Proof Explorer

Theorem icombl1

Description: A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion icombl1 ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2 pnfxr ⊢ +∞ ∈ ℝ*
3 2 a1i ⊢ ( 𝐴 ∈ ℝ → +∞ ∈ ℝ* )
4 ltpnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 < +∞ )
5 snunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 < +∞ ) → ( { 𝐴 } ∪ ( 𝐴 (,) +∞ ) ) = ( 𝐴 [,) +∞ ) )
6 1 3 4 5 syl3anc ⊢ ( 𝐴 ∈ ℝ → ( { 𝐴 } ∪ ( 𝐴 (,) +∞ ) ) = ( 𝐴 [,) +∞ ) )
7 snssi ⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ⊆ ℝ )
8 ovolsn ⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ { 𝐴 } ) = 0 )
9 nulmbl ⊢ ( ( { 𝐴 } ⊆ ℝ ∧ ( vol* ‘ { 𝐴 } ) = 0 ) → { 𝐴 } ∈ dom vol )
10 7 8 9 syl2anc ⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ∈ dom vol )
11 ioombl1 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 (,) +∞ ) ∈ dom vol )
12 1 11 syl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 (,) +∞ ) ∈ dom vol )
13 unmbl ⊢ ( ( { 𝐴 } ∈ dom vol ∧ ( 𝐴 (,) +∞ ) ∈ dom vol ) → ( { 𝐴 } ∪ ( 𝐴 (,) +∞ ) ) ∈ dom vol )
14 10 12 13 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( { 𝐴 } ∪ ( 𝐴 (,) +∞ ) ) ∈ dom vol )
15 6 14 eqeltrrd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ∈ dom vol )