Step |
Hyp |
Ref |
Expression |
1 |
|
iooss1 |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐶 ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐵 (,) 𝐷 ) ) |
2 |
1
|
ad4ant24 |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐵 (,) 𝐷 ) ) |
3 |
|
ioossicc |
⊢ ( 𝐵 (,) 𝐷 ) ⊆ ( 𝐵 [,] 𝐷 ) |
4 |
2 3
|
sstrdi |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐵 [,] 𝐷 ) ) |
5 |
|
sslin |
⊢ ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐵 [,] 𝐷 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) ⊆ ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,] 𝐷 ) ) ) |
6 |
4 5
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) ⊆ ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,] 𝐷 ) ) ) |
7 |
|
simplll |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → 𝐴 ∈ ℝ* ) |
8 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ℝ* ) |
9 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → 𝐷 ∈ ℝ* ) |
10 |
|
df-ioo |
⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } ) |
11 |
|
df-icc |
⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ) |
12 |
|
xrlenlt |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐵 ) ) |
13 |
10 11 12
|
ixxdisj |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,] 𝐷 ) ) = ∅ ) |
14 |
7 8 9 13
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,] 𝐷 ) ) = ∅ ) |
15 |
6 14
|
sseqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) ⊆ ∅ ) |
16 |
|
ss0 |
⊢ ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) ⊆ ∅ → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ∅ ) |
17 |
15 16
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ∅ ) |