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	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to [A, B] \cap [C, D] = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to A \in ℝ^{*}$
2		simp3	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to B < C$
3		ltrelxr	$⊢ < \subseteq ℝ^{} \times ℝ^{}$
4	3	brel	$⊢ B < C \to (B \in ℝ^{} \land C \in ℝ^{})$
5	2 4	syl	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to (B \in ℝ^{} \land C \in ℝ^{})$
6	5	simprd	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to C \in ℝ^{*}$
7	1	xrleidd	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to A \leq A$
8		iccssico	$⊢ ((A \in ℝ^{} \land C \in ℝ^{}) \land (A \leq A \land B < C)) \to [A, B] \subseteq [A, C)$
9	1 6 7 2 8	syl22anc	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to [A, B] \subseteq [A, C)$
10		simp2	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to D \in ℝ^{*}$
11		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
12		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
13		xrlenlt	$⊢ (C \in ℝ^{} \land w \in ℝ^{}) \to (C \leq w \leftrightarrow \neg w < C)$
14	11 12 13	ixxdisj	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land D \in ℝ^{*}) \to [A, C) \cap [C, D] = \emptyset$
15	1 6 10 14	syl3anc	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to [A, C) \cap [C, D] = \emptyset$
16	9 15	ssdisjd	$⊢ (A \in ℝ^{} \land D \in ℝ^{} \land B < C) \to [A, B] \cap [C, D] = \emptyset$