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

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