ioondisj2

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

		Ref	Expression
	Assertion	ioondisj2	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq 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 < D \land D \leq 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 < D \land D \leq 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 < D \land D \leq 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 < D \land D \leq 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 < D \land D \leq B)) \to (A, B) \cap (C, D) = (if (A \leq C, C, A), if (B \leq D, B, D))$
7		simprr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to D \leq B$
8		xrmineq	$⊢ (B \in ℝ^{} \land D \in ℝ^{} \land D \leq B) \to if (B \leq D, B, D) = D$
9	2 4 7 8	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to if (B \leq D, B, D) = D$
10	9	oveq2d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to (if (A \leq C, C, A), if (B \leq D, B, D)) = (if (A \leq C, C, A), D)$
11		simpr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land A \leq C) \to A \leq C$
12	11	iftrued	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land A \leq C) \to if (A \leq C, C, A) = C$
13		simplr3	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to C < D$
14	13	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land A \leq C) \to C < D$
15	12 14	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land A \leq C) \to if (A \leq C, C, A) < D$
16		simpr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land \neg A \leq C) \to \neg A \leq C$
17	16	iffalsed	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land \neg A \leq C) \to if (A \leq C, C, A) = A$
18		simplrl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land \neg A \leq C) \to A < D$
19	17 18	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \land \neg A \leq C) \to if (A \leq C, C, A) < D$
20	15 19	pm2.61dan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to if (A \leq C, C, A) < D$
21	3 1	ifcld	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to if (A \leq C, C, A) \in ℝ^{*}$
22		ioon0	$⊢ (if (A \leq C, C, A) \in ℝ^{} \land D \in ℝ^{}) \to ((if (A \leq C, C, A), D) \neq \emptyset \leftrightarrow if (A \leq C, C, A) < D)$
23	21 4 22	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to ((if (A \leq C, C, A), D) \neq \emptyset \leftrightarrow if (A \leq C, C, A) < D)$
24	20 23	mpbird	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to (if (A \leq C, C, A), D) \neq \emptyset$
25	10 24	eqnetrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to (if (A \leq C, C, A), if (B \leq D, B, D)) \neq \emptyset$
26	6 25	eqnetrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land (C \in ℝ^{} \land D \in ℝ^{} \land C < D)) \land (A < D \land D \leq B)) \to (A, B) \cap (C, D) \neq \emptyset$

Metamath Proof Explorer

Theorem ioondisj2

Proof