elxr

Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005)

		Ref	Expression
	Assertion	elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$

Step	Hyp	Ref	Expression
1		df-xr	$⊢ ℝ^{*} = ℝ \cup \{+∞, −∞\}$
2	1	eleq2i	$⊢ A \in ℝ^{*} \leftrightarrow A \in (ℝ \cup \{+∞, −∞\})$
3		elun	$⊢ A \in (ℝ \cup \{+∞, −∞\}) \leftrightarrow (A \in ℝ \lor A \in \{+∞, −∞\})$
4		pnfex	$⊢ +∞ \in V$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6	5	elexi	$⊢ −∞ \in V$
7	4 6	elpr2	$⊢ A \in \{+∞, −∞\} \leftrightarrow (A = +∞ \lor A = −∞)$
8	7	orbi2i	$⊢ (A \in ℝ \lor A \in \{+∞, −∞\}) \leftrightarrow (A \in ℝ \lor (A = +∞ \lor A = −∞))$
9		3orass	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \leftrightarrow (A \in ℝ \lor (A = +∞ \lor A = −∞))$
10	8 9	bitr4i	$⊢ (A \in ℝ \lor A \in \{+∞, −∞\}) \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
11	2 3 10	3bitri	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$

Metamath Proof Explorer