# Metamath Proof Explorer

## Theorem elxr

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

Ref Expression
Assertion elxr ${⊢}{A}\in {ℝ}^{*}↔\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 {ℝ}^{*}↔{A}\in \left(ℝ\cup \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}\right)$
3 elun ${⊢}{A}\in \left(ℝ\cup \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}\right)↔\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\}↔\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)↔\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)↔\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)↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)$
11 2 3 10 3bitri ${⊢}{A}\in {ℝ}^{*}↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)$