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