ixxdisj

Description: Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014)

	Ref	Expression
Hypotheses	ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
	ixxun.2	$⊢ P = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x T z \land z U y)\})$
	ixxun.3	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B T w \leftrightarrow \neg w S B)$
Assertion	ixxdisj	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A O B) \cap (B P C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
2		ixxun.2	$⊢ P = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x T z \land z U y)\})$
3		ixxun.3	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B T w \leftrightarrow \neg w S B)$
4		elin	$⊢ w \in ((A O B) \cap (B P C)) \leftrightarrow (w \in (A O B) \land w \in (B P C))$
5	1	elixx1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (w \in (A O B) \leftrightarrow (w \in ℝ^{*} \land A R w \land w S B))$
6	5	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (w \in (A O B) \leftrightarrow (w \in ℝ^{} \land A R w \land w S B))$
7	6	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land w \in (A O B)) \to (w \in ℝ^{} \land A R w \land w S B)$
8	7	simp3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land w \in (A O B)) \to w S B$
9	8	adantrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (w \in (A O B) \land w \in (B P C))) \to w S B$
10	2	elixx1	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (w \in (B P C) \leftrightarrow (w \in ℝ^{*} \land B T w \land w U C))$
11	10	3adant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \to (w \in (B P C) \leftrightarrow (w \in ℝ^{} \land B T w \land w U C))$
12	11	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land w \in (B P C)) \to (w \in ℝ^{} \land B T w \land w U C)$
13	12	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land w \in (B P C)) \to B T w$
14		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land w \in (B P C)) \to B \in ℝ^{}$
15	12	simp1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land w \in (B P C)) \to w \in ℝ^{}$
16	14 15 3	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land w \in (B P C)) \to (B T w \leftrightarrow \neg w S B)$
17	13 16	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land w \in (B P C)) \to \neg w S B$
18	17	adantrl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (w \in (A O B) \land w \in (B P C))) \to \neg w S B$
19	9 18	pm2.65da	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to \neg (w \in (A O B) \land w \in (B P C))$
20	19	pm2.21d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((w \in (A O B) \land w \in (B P C)) \to w \in \emptyset)$
21	4 20	biimtrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (w \in ((A O B) \cap (B P C)) \to w \in \emptyset)$
22	21	ssrdv	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A O B) \cap (B P C) \subseteq \emptyset$
23		ss0	$⊢ (A O B) \cap (B P C) \subseteq \emptyset \to (A O B) \cap (B P C) = \emptyset$
24	22 23	syl	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A O B) \cap (B P C) = \emptyset$

Metamath Proof Explorer

Theorem ixxdisj

Proof