Metamath Proof Explorer


Theorem iccdisj2

Description: If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Assertion iccdisj2 ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → 𝐴 ∈ ℝ* )
2 simp3 ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → 𝐵 < 𝐶 )
3 ltrelxr < ⊆ ( ℝ* × ℝ* )
4 3 brel ( 𝐵 < 𝐶 → ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) )
5 2 4 syl ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) )
6 5 simprd ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
7 1 xrleidd ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → 𝐴𝐴 )
8 iccssico ( ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ ( 𝐴𝐴𝐵 < 𝐶 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) 𝐶 ) )
9 1 6 7 2 8 syl22anc ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,) 𝐶 ) )
10 simp2 ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → 𝐷 ∈ ℝ* )
11 df-ico [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
12 df-icc [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧𝑦 ) } )
13 xrlenlt ( ( 𝐶 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 𝐶𝑤 ↔ ¬ 𝑤 < 𝐶 ) )
14 11 12 13 ixxdisj ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝐷 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐶 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ )
15 1 6 10 14 syl3anc ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → ( ( 𝐴 [,) 𝐶 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ )
16 9 15 ssdisjd ( ( 𝐴 ∈ ℝ*𝐷 ∈ ℝ*𝐵 < 𝐶 ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐶 [,] 𝐷 ) ) = ∅ )