elioopnf

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

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

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

Metamath Proof Explorer