icodisj

Description: Adjacent left-closed right-open real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014)

		Ref	Expression
	Assertion	icodisj	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to [A, B) \cap [B, C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in ([A, B) \cap [B, C)) \leftrightarrow (x \in [A, B) \land x \in [B, C))$
2		elico1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (x \in [A, B) \leftrightarrow (x \in ℝ^{*} \land A \leq x \land x < B))$
3	2	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (x \in [A, B) \leftrightarrow (x \in ℝ^{} \land A \leq x \land x < B))$
4	3	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land x \in [A, B)) \to (x \in ℝ^{} \land A \leq x \land x < B)$
5	4	simp3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land x \in [A, B)) \to x < B$
6	5	adantrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B) \land x \in [B, C))) \to x < B$
7		elico1	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (x \in [B, C) \leftrightarrow (x \in ℝ^{*} \land B \leq x \land x < C))$
8	7	3adant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (x \in [B, C) \leftrightarrow (x \in ℝ^{} \land B \leq x \land x < C))$
9	8	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land x \in [B, C)) \to (x \in ℝ^{} \land B \leq x \land x < C)$
10	9	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land x \in [B, C)) \to B \leq x$
11		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land x \in [B, C)) \to B \in ℝ^{}$
12	9	simp1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land x \in [B, C)) \to x \in ℝ^{}$
13	11 12	xrlenltd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land x \in [B, C)) \to (B \leq x \leftrightarrow \neg x < B)$
14	10 13	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land x \in [B, C)) \to \neg x < B$
15	14	adantrl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (x \in [A, B) \land x \in [B, C))) \to \neg x < B$
16	6 15	pm2.65da	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to \neg (x \in [A, B) \land x \in [B, C))$
17	16	pm2.21d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((x \in [A, B) \land x \in [B, C)) \to x \in \emptyset)$
18	1 17	biimtrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (x \in ([A, B) \cap [B, C)) \to x \in \emptyset)$
19	18	ssrdv	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to [A, B) \cap [B, C) \subseteq \emptyset$
20		ss0	$⊢ [A, B) \cap [B, C) \subseteq \emptyset \to [A, B) \cap [B, C) = \emptyset$
21	19 20	syl	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to [A, B) \cap [B, C) = \emptyset$

Metamath Proof Explorer

Theorem icodisj

Proof