ico0

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

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

Proof

Step	Hyp	Ref	Expression
1		icoval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to [A, B) = \{x \in ℝ^{*} \| (A \leq x \land x < B)\}$
2	1	eqeq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B) = \emptyset \leftrightarrow \{x \in ℝ^{*} \| (A \leq x \land x < B)\} = \emptyset)$
3		df-ne	$⊢ \{x \in ℝ^{} \| (A \leq x \land x < B)\} \neq \emptyset \leftrightarrow \neg \{x \in ℝ^{} \| (A \leq x \land x < B)\} = \emptyset$
4		rabn0	$⊢ \{x \in ℝ^{} \| (A \leq x \land x < B)\} \neq \emptyset \leftrightarrow \exists x \in ℝ^{} (A \leq x \land x < B)$
5	3 4	bitr3i	$⊢ \neg \{x \in ℝ^{} \| (A \leq x \land x < B)\} = \emptyset \leftrightarrow \exists x \in ℝ^{} (A \leq x \land x < B)$
6		xrlelttr	$⊢ (A \in ℝ^{} \land x \in ℝ^{} \land B \in ℝ^{*}) \to ((A \leq x \land x < B) \to A < B)$
7	6	3com23	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \to ((A \leq x \land x < B) \to A < B)$
8	7	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℝ^{*}) \to ((A \leq x \land x < B) \to A < B)$
9	8	rexlimdva	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A \leq x \land x < B) \to A < B)$
10		qbtwnxr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists x \in ℚ (A < x \land x < B)$
11		qre	$⊢ x \in ℚ \to x \in ℝ$
12	11	rexrd	$⊢ x \in ℚ \to x \in ℝ^{*}$
13	12	a1i	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{} \land A < B)) \to (x \in ℚ \to x \in ℝ^{})$
14		simpr1	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{} \land A < B)) \to A \in ℝ^{}$
15		simpl	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{} \land A < B)) \to x \in ℝ^{}$
16		xrltle	$⊢ (A \in ℝ^{} \land x \in ℝ^{}) \to (A < x \to A \leq x)$
17	14 15 16	syl2anc	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{*} \land A < B)) \to (A < x \to A \leq x)$
18	17	anim1d	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{*} \land A < B)) \to ((A < x \land x < B) \to (A \leq x \land x < B))$
19	13 18	anim12d	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{} \land A < B)) \to ((x \in ℚ \land (A < x \land x < B)) \to (x \in ℝ^{} \land (A \leq x \land x < B)))$
20	19	ex	$⊢ x \in ℝ^{} \to ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((x \in ℚ \land (A < x \land x < B)) \to (x \in ℝ^{} \land (A \leq x \land x < B))))$
21	12 20	syl	$⊢ x \in ℚ \to ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((x \in ℚ \land (A < x \land x < B)) \to (x \in ℝ^{*} \land (A \leq x \land x < B))))$
22	21	adantr	$⊢ (x \in ℚ \land (A < x \land x < B)) \to ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((x \in ℚ \land (A < x \land x < B)) \to (x \in ℝ^{*} \land (A \leq x \land x < B))))$
23	22	pm2.43b	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((x \in ℚ \land (A < x \land x < B)) \to (x \in ℝ^{*} \land (A \leq x \land x < B)))$
24	23	reximdv2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (\exists x \in ℚ (A < x \land x < B) \to \exists x \in ℝ^{*} (A \leq x \land x < B))$
25	10 24	mpd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists x \in ℝ^{*} (A \leq x \land x < B)$
26	25	3expia	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \exists x \in ℝ^{*} (A \leq x \land x < B))$
27	9 26	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A \leq x \land x < B) \leftrightarrow A < B)$
28	5 27	bitrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A \leq x \land x < B)\} = \emptyset \leftrightarrow A < B)$
29		xrltnle	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \leftrightarrow \neg B \leq A)$
30	28 29	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A \leq x \land x < B)\} = \emptyset \leftrightarrow \neg B \leq A)$
31	30	con4bid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\{x \in ℝ^{*} \| (A \leq x \land x < B)\} = \emptyset \leftrightarrow B \leq A)$
32	2 31	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B) = \emptyset \leftrightarrow B \leq A)$

Metamath Proof Explorer

Theorem ico0

Proof