Metamath Proof Explorer

Theorem ioodisj

Description: If the upper bound of one open interval is less than or equal to the lower bound of the other, the intervals are disjoint. (Contributed by Jeff Hankins, 13-Jul-2009)

Ref Expression
Assertion ioodisj ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → A B ∩ C D = ∅

Proof

Step Hyp Ref Expression
1 iooss1 ⊢ B ∈ ℝ * ∧ B ≤ C → C D ⊆ B D
2 1 ad4ant24 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → C D ⊆ B D
3 ioossicc ⊢ B D ⊆ B D
4 2 3 sstrdi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → C D ⊆ B D
5 sslin ⊢ C D ⊆ B D → A B ∩ C D ⊆ A B ∩ B D
6 4 5 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → A B ∩ C D ⊆ A B ∩ B D
7 simplll ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → A ∈ ℝ *
8 simpllr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → B ∈ ℝ *
9 simplrr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → D ∈ ℝ *
10 df-ioo ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x < z ∧ z < y
11 df-icc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z ≤ y
12 xrlenlt ⊢ B ∈ ℝ * ∧ w ∈ ℝ * → B ≤ w ↔ ¬ w < B
13 10 11 12 ixxdisj ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ D ∈ ℝ * → A B ∩ B D = ∅
14 7 8 9 13 syl3anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → A B ∩ B D = ∅
15 6 14 sseqtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → A B ∩ C D ⊆ ∅
16 ss0 ⊢ A B ∩ C D ⊆ ∅ → A B ∩ C D = ∅
17 15 16 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ D ∈ ℝ * ∧ B ≤ C → A B ∩ C D = ∅