Theorem elxr 9346

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 7623	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2161	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3156	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 7638	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 7641	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2645	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3488	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 717	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 930	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 186	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 205	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 104   ∨ wo 667   ∨ w3o 926   = wceq 1296   ∈ wcel 1445   ∪ cun 3011  {cpr 3467  ℝcr 7446  +∞cpnf 7616  -∞cmnf 7617  ℝ^*cxr 7618

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-un 4284  ax-cnex 7533

This theorem depends on definitions:  df-bi 116  df-3or 928  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-uni 3676  df-pnf 7621  df-mnf 7622  df-xr 7623

This theorem is referenced by:  xrnemnf  9347  xrnepnf  9348  xrltnr  9349  xrltnsym  9362  xrlttr  9364  xrltso  9365  xrlttri3  9366  nltpnft  9380  npnflt  9381  ngtmnft  9383  nmnfgt  9384  xrrebnd  9385  xnegcl  9398  xnegneg  9399  xltnegi  9401  xrpnfdc  9408  xrmnfdc  9409  xnegid  9425  xaddcom  9427  xaddid1  9428  xnegdi  9434  xleadd1a  9439  xltadd1  9442  xlt2add  9446  xsubge0  9447  xposdif  9448  xleaddadd  9453  qbtwnxr  9818  xrmaxiflemcl  10788  xrmaxifle  10789  xrmaxiflemab  10790  xrmaxiflemlub  10791  xrmaxltsup  10801  xrmaxadd  10804  xrbdtri  10819  isxmet2d  12134  blssioo  12319