ioc0

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

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

Proof

Step	Hyp	Ref	Expression
1		iocval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B] = \{x \in ℝ^{*} \| (A < x \land x \leq B)\}$
2	1	eqeq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B] = \emptyset \leftrightarrow \{x \in ℝ^{*} \| (A < x \land x \leq B)\} = \emptyset)$
3		df-ne	$⊢ \{x \in ℝ^{} \| (A < x \land x \leq B)\} \neq \emptyset \leftrightarrow \neg \{x \in ℝ^{} \| (A < x \land x \leq B)\} = \emptyset$
4		rabn0	$⊢ \{x \in ℝ^{} \| (A < x \land x \leq B)\} \neq \emptyset \leftrightarrow \exists x \in ℝ^{} (A < x \land x \leq B)$
5	3 4	bitr3i	$⊢ \neg \{x \in ℝ^{} \| (A < x \land x \leq B)\} = \emptyset \leftrightarrow \exists x \in ℝ^{} (A < x \land x \leq B)$
6		xrltletr	$⊢ (A \in ℝ^{} \land x \in ℝ^{} \land B \in ℝ^{*}) \to ((A < x \land x \leq B) \to A < B)$
7	6	3com23	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \to ((A < x \land x \leq B) \to A < B)$
8	7	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℝ^{*}) \to ((A < x \land x \leq B) \to A < B)$
9	8	rexlimdva	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A < x \land x \leq 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		xrltle	$⊢ (x \in ℝ^{} \land B \in ℝ^{}) \to (x < B \to x \leq B)$
15	14	3ad2antr2	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{*} \land A < B)) \to (x < B \to x \leq B)$
16	15	anim2d	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{*} \land A < B)) \to ((A < x \land x < B) \to (A < x \land x \leq B))$
17	13 16	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 < x \land x \leq B)))$
18	17	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 < x \land x \leq B))))$
19	12 18	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 < x \land x \leq B))))$
20	19	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 < x \land x \leq B))))$
21	20	pm2.43b	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to ((x \in ℚ \land (A < x \land x < B)) \to (x \in ℝ^{*} \land (A < x \land x \leq B)))$
22	21	reximdv2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (\exists x \in ℚ (A < x \land x < B) \to \exists x \in ℝ^{*} (A < x \land x \leq B))$
23	10 22	mpd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists x \in ℝ^{*} (A < x \land x \leq B)$
24	23	3expia	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \exists x \in ℝ^{*} (A < x \land x \leq B))$
25	9 24	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℝ^{*} (A < x \land x \leq B) \leftrightarrow A < B)$
26	5 25	bitrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A < x \land x \leq B)\} = \emptyset \leftrightarrow A < B)$
27		xrltnle	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \leftrightarrow \neg B \leq A)$
28	26 27	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg \{x \in ℝ^{*} \| (A < x \land x \leq B)\} = \emptyset \leftrightarrow \neg B \leq A)$
29	28	con4bid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\{x \in ℝ^{*} \| (A < x \land x \leq B)\} = \emptyset \leftrightarrow B \leq A)$
30	2 29	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B] = \emptyset \leftrightarrow B \leq A)$

Metamath Proof Explorer

Theorem ioc0

Proof