Step |
Hyp |
Ref |
Expression |
1 |
|
iccssre |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
2 |
|
dfss4 |
⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ↔ ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) = ( 𝐴 [,] 𝐵 ) ) |
3 |
1 2
|
sylib |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) = ( 𝐴 [,] 𝐵 ) ) |
4 |
|
difreicc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) = ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) ) |
5 |
|
ioombl |
⊢ ( -∞ (,) 𝐴 ) ∈ dom vol |
6 |
|
ioombl |
⊢ ( 𝐵 (,) +∞ ) ∈ dom vol |
7 |
|
unmbl |
⊢ ( ( ( -∞ (,) 𝐴 ) ∈ dom vol ∧ ( 𝐵 (,) +∞ ) ∈ dom vol ) → ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) ∈ dom vol ) |
8 |
5 6 7
|
mp2an |
⊢ ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) ∈ dom vol |
9 |
4 8
|
eqeltrdi |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ∈ dom vol ) |
10 |
|
cmmbl |
⊢ ( ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ∈ dom vol → ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ∈ dom vol ) |
11 |
9 10
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ∈ dom vol ) |
12 |
3 11
|
eqeltrrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ dom vol ) |