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→AB∩CD=∅

Proof

Step Hyp Ref Expression
1 iooss1 ⊢B∈ℝ*∧B≤C→CD⊆BD
2 1 ad4ant24 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*∧B≤C→CD⊆BD
3 ioossicc ⊢BD⊆BD
4 2 3 sstrdi ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*∧B≤C→CD⊆BD
5 sslin ⊢CD⊆BD→AB∩CD⊆AB∩BD
6 4 5 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*∧B≤C→AB∩CD⊆AB∩BD
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∈ℝ*→AB∩BD=∅
14 7 8 9 13 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*∧B≤C→AB∩BD=∅
15 6 14 sseqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*∧B≤C→AB∩CD⊆∅
16 ss0 ⊢AB∩CD⊆∅→AB∩CD=∅
17 15 16 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*∧B≤C→AB∩CD=∅