icc0

Description: An empty closed interval of extended reals. (Contributed by FL, 30-May-2014)

		Ref	Expression
	Assertion	icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$

Proof

Step	Hyp	Ref	Expression
1		iccval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B] = \{x \in ℝ^{*} \| (A \leq x \land x \leq B)\}$
2	1	eqeq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow \{x \in ℝ^{*} \| (A \leq x \land x \leq B)\} = \emptyset)$
3		df-ne	$⊢ \{x \in ℝ^{} \| (A \leq x \land x \leq B)\} \neq \emptyset \leftrightarrow \neg \{x \in ℝ^{} \| (A \leq x \land x \leq B)\} = \emptyset$
4		rabn0	$⊢ \{x \in ℝ^{} \| (A \leq x \land x \leq B)\} \neq \emptyset \leftrightarrow \exists x \in ℝ^{} (A \leq x \land x \leq B)$
5	3 4	bitr3i	$⊢ \neg \{x \in ℝ^{} \| (A \leq x \land x \leq B)\} = \emptyset \leftrightarrow \exists x \in ℝ^{} (A \leq x \land x \leq B)$
6		xrletr	$⊢ (A \in ℝ^{} \land x \in ℝ^{} \land B \in ℝ^{*}) \to ((A \leq x \land x \leq B) \to A \leq B)$
7	6	3com23	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \to ((A \leq x \land x \leq B) \to A \leq B)$
8	7	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℝ^{*}) \to ((A \leq x \land x \leq B) \to A \leq B)$
9	8	rexlimdva	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A \leq x \land x \leq B) \to A \leq B)$
10		simp2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in ℝ^{*}$
11		simp3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \leq B$
12		xrleid	$⊢ B \in ℝ^{*} \to B \leq B$
13	12	3ad2ant2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \leq B$
14		breq2	$⊢ x = B \to (A \leq x \leftrightarrow A \leq B)$
15		breq1	$⊢ x = B \to (x \leq B \leftrightarrow B \leq B)$
16	14 15	anbi12d	$⊢ x = B \to ((A \leq x \land x \leq B) \leftrightarrow (A \leq B \land B \leq B))$
17	16	rspcev	$⊢ (B \in ℝ^{} \land (A \leq B \land B \leq B)) \to \exists x \in ℝ^{} (A \leq x \land x \leq B)$
18	10 11 13 17	syl12anc	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to \exists x \in ℝ^{*} (A \leq x \land x \leq B)$
19	18	3expia	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \to \exists x \in ℝ^{*} (A \leq x \land x \leq B))$
20	9 19	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A \leq x \land x \leq B) \leftrightarrow A \leq B)$
21	5 20	bitrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A \leq x \land x \leq B)\} = \emptyset \leftrightarrow A \leq B)$
22		xrlenlt	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \leftrightarrow \neg B < A)$
23	21 22	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A \leq x \land x \leq B)\} = \emptyset \leftrightarrow \neg B < A)$
24	23	con4bid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\{x \in ℝ^{*} \| (A \leq x \land x \leq B)\} = \emptyset \leftrightarrow B < A)$
25	2 24	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$

Metamath Proof Explorer

Theorem icc0

Proof