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	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ∅ )

Proof

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	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ∅ )