Theorem elxr 9980

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 8193	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2296	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3345	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8208	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8211	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2812	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3688	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 767	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1005	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 187	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 206	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 105   ∨ wo 713   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200   ∪ cun 3195  {cpr 3667  ℝcr 8006  +∞cpnf 8186  -∞cmnf 8187  ℝ^*cxr 8188

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-un 4524  ax-cnex 8098

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3889  df-pnf 8191  df-mnf 8192  df-xr 8193

This theorem is referenced by:  xrnemnf  9981  xrnepnf  9982  xrltnr  9983  xrltnsym  9997  xrlttr  9999  xrltso  10000  xrlttri3  10001  nltpnft  10018  npnflt  10019  ngtmnft  10021  nmnfgt  10022  xrrebnd  10023  xnegcl  10036  xnegneg  10037  xltnegi  10039  xrpnfdc  10046  xrmnfdc  10047  xnegid  10063  xaddcom  10065  xaddid1  10066  xnegdi  10072  xleadd1a  10077  xltadd1  10080  xlt2add  10084  xsubge0  10085  xposdif  10086  xleaddadd  10091  qbtwnxr  10485  xrmaxiflemcl  11764  xrmaxifle  11765  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxltsup  11777  xrmaxadd  11780  xrbdtri  11795  isxmet2d  15030  blssioo  15235