Theorem elxr 10016

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

Assertion

Ref	Expression
elxr	⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Proof of Theorem elxr

Step	Hyp	Ref	Expression
1		df-xr 8223	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2297	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3347	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8238	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8241	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2814	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3692	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 769	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1007	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 187	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 206	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 105   ∨ wo 715   ∨ w3o 1003   = wceq 1397   ∈ wcel 2201   ∪ cun 3197  {cpr 3671  ℝcr 8036  +∞cpnf 8216  -∞cmnf 8217  ℝ^*cxr 8218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-un 4532  ax-cnex 8128

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rex 2515  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-uni 3895  df-pnf 8221  df-mnf 8222  df-xr 8223

This theorem is referenced by:  xrnemnf  10017  xrnepnf  10018  xrltnr  10019  xrltnsym  10033  xrlttr  10035  xrltso  10036  xrlttri3  10037  nltpnft  10054  npnflt  10055  ngtmnft  10057  nmnfgt  10058  xrrebnd  10059  xnegcl  10072  xnegneg  10073  xltnegi  10075  xrpnfdc  10082  xrmnfdc  10083  xnegid  10099  xaddcom  10101  xaddid1  10102  xnegdi  10108  xleadd1a  10113  xltadd1  10116  xlt2add  10120  xsubge0  10121  xposdif  10122  xleaddadd  10127  qbtwnxr  10523  xrmaxiflemcl  11828  xrmaxifle  11829  xrmaxiflemab  11830  xrmaxiflemlub  11831  xrmaxltsup  11841  xrmaxadd  11844  xrbdtri  11859  isxmet2d  15101  blssioo  15306