ioo0

Description: An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		iooval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \{x \in ℝ^{*} \| (A < x \land x < B)\}$
2	1	eqeq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow \{x \in ℝ^{*} \| (A < x \land x < B)\} = \emptyset)$
3		df-ne	$⊢ \{x \in ℝ^{} \| (A < x \land x < B)\} \neq \emptyset \leftrightarrow \neg \{x \in ℝ^{} \| (A < x \land x < B)\} = \emptyset$
4		rabn0	$⊢ \{x \in ℝ^{} \| (A < x \land x < B)\} \neq \emptyset \leftrightarrow \exists x \in ℝ^{} (A < x \land x < B)$
5	3 4	bitr3i	$⊢ \neg \{x \in ℝ^{} \| (A < x \land x < B)\} = \emptyset \leftrightarrow \exists x \in ℝ^{} (A < x \land x < B)$
6		xrlttr	$⊢ (A \in ℝ^{} \land x \in ℝ^{} \land B \in ℝ^{*}) \to ((A < x \land x < B) \to A < B)$
7	6	3com23	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \to ((A < x \land x < B) \to A < B)$
8	7	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℝ^{*}) \to ((A < x \land x < B) \to A < B)$
9	8	rexlimdva	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A < 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	anim1i	$⊢ (x \in ℚ \land (A < x \land x < B)) \to (x \in ℝ^{*} \land (A < x \land x < B))$
14	13	reximi2	$⊢ \exists x \in ℚ (A < x \land x < B) \to \exists x \in ℝ^{*} (A < x \land x < B)$
15	10 14	syl	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists x \in ℝ^{*} (A < x \land x < B)$
16	15	3expia	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \exists x \in ℝ^{*} (A < x \land x < B))$
17	9 16	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A < x \land x < B) \leftrightarrow A < B)$
18	5 17	bitrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A < x \land x < B)\} = \emptyset \leftrightarrow A < B)$
19		xrltnle	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \leftrightarrow \neg B \leq A)$
20	18 19	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A < x \land x < B)\} = \emptyset \leftrightarrow \neg B \leq A)$
21	20	con4bid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\{x \in ℝ^{*} \| (A < x \land x < B)\} = \emptyset \leftrightarrow B \leq A)$
22	2 21	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$

Metamath Proof Explorer

Theorem ioo0

Proof