ioon0

Description: An open interval of extended reals is nonempty iff the lower argument is less than the upper argument. (Contributed by NM, 2-Mar-2007)

		Ref	Expression
	Assertion	ioon0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) \neq \emptyset \leftrightarrow A < B)$

Proof

Step	Hyp	Ref	Expression
1		ioo0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
2		xrlenlt	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B \leq A \leftrightarrow \neg A < B)$
3	2	ancoms	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B \leq A \leftrightarrow \neg A < B)$
4	1 3	bitr2d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg A < B \leftrightarrow (A, B) = \emptyset)$
5	4	necon1abid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) \neq \emptyset \leftrightarrow A < B)$

Metamath Proof Explorer

Theorem ioon0

Proof