ioondisj1

Description: A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	ioondisj1	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (A, B) \cap (C, D) \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		simpll1	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to A \in ℝ^{*}$
2		simpll2	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to B \in ℝ^{*}$
3		simplr1	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to C \in ℝ^{*}$
4		simplr2	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to D \in ℝ^{*}$
5		iooin	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \to (A, B) \cap (C, D) = (if (A \leq C, C, A), if (B \leq D, B, D))$
6	1 2 3 4 5	syl22anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (A, B) \cap (C, D) = (if (A \leq C, C, A), if (B \leq D, B, D))$
7		simprl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to A \leq C$
8	7	iftrued	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to if (A \leq C, C, A) = C$
9	8	oveq1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (if (A \leq C, C, A), if (B \leq D, B, D)) = (C, if (B \leq D, B, D))$
10		simprr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to C < B$
11		simplr3	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to C < D$
12	10 11	jca	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (C < B \land C < D)$
13		xrltmin	$⊢ (C \in ℝ^{} \land B \in ℝ^{} \land D \in ℝ^{*}) \to (C < if (B \leq D, B, D) \leftrightarrow (C < B \land C < D))$
14	3 2 4 13	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (C < if (B \leq D, B, D) \leftrightarrow (C < B \land C < D))$
15	12 14	mpbird	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to C < if (B \leq D, B, D)$
16	2 4	ifcld	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to if (B \leq D, B, D) \in ℝ^{*}$
17		ioon0	$⊢ (C \in ℝ^{} \land if (B \leq D, B, D) \in ℝ^{}) \to ((C, if (B \leq D, B, D)) \neq \emptyset \leftrightarrow C < if (B \leq D, B, D))$
18	3 16 17	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to ((C, if (B \leq D, B, D)) \neq \emptyset \leftrightarrow C < if (B \leq D, B, D))$
19	15 18	mpbird	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (C, if (B \leq D, B, D)) \neq \emptyset$
20	9 19	eqnetrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (if (A \leq C, C, A), if (B \leq D, B, D)) \neq \emptyset$
21	6 20	eqnetrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A \leq C \land C < B)) \to (A, B) \cap (C, D) \neq \emptyset$

Metamath Proof Explorer

Theorem ioondisj1

Proof