elioomnf

Description: Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014)

		Ref	Expression
	Assertion	elioomnf	$⊢ A \in ℝ^{*} \to (B \in (−∞, A) \leftrightarrow (B \in ℝ \land B < A))$

Step	Hyp	Ref	Expression
1		mnfxr	$⊢ −∞ \in ℝ^{*}$
2		elioo2	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to (B \in (−∞, A) \leftrightarrow (B \in ℝ \land −∞ < B \land B < A))$
3	1 2	mpan	$⊢ A \in ℝ^{*} \to (B \in (−∞, A) \leftrightarrow (B \in ℝ \land −∞ < B \land B < A))$
4		an32	$⊢ ((B \in ℝ \land −∞ < B) \land B < A) \leftrightarrow ((B \in ℝ \land B < A) \land −∞ < B)$
5		df-3an	$⊢ (B \in ℝ \land −∞ < B \land B < A) \leftrightarrow ((B \in ℝ \land −∞ < B) \land B < A)$
6		mnflt	$⊢ B \in ℝ \to −∞ < B$
7	6	adantr	$⊢ (B \in ℝ \land B < A) \to −∞ < B$
8	7	pm4.71i	$⊢ (B \in ℝ \land B < A) \leftrightarrow ((B \in ℝ \land B < A) \land −∞ < B)$
9	4 5 8	3bitr4i	$⊢ (B \in ℝ \land −∞ < B \land B < A) \leftrightarrow (B \in ℝ \land B < A)$
10	3 9	bitrdi	$⊢ A \in ℝ^{*} \to (B \in (−∞, A) \leftrightarrow (B \in ℝ \land B < A))$

Metamath Proof Explorer