Theorem elxr

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

	Ref	Expression
Assertion	elxr	$$⊢A\in {ℝ}^{*}\leftrightarrow \left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)$$

Proof

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