Theorem elxr 9989

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 8201	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2296	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3345	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8216	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8219	. . . . . 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 8014  +∞cpnf 8194  -∞cmnf 8195  ℝ^*cxr 8196

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 4259  ax-un 4525  ax-cnex 8106

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 8199  df-mnf 8200  df-xr 8201

This theorem is referenced by:  xrnemnf  9990  xrnepnf  9991  xrltnr  9992  xrltnsym  10006  xrlttr  10008  xrltso  10009  xrlttri3  10010  nltpnft  10027  npnflt  10028  ngtmnft  10030  nmnfgt  10031  xrrebnd  10032  xnegcl  10045  xnegneg  10046  xltnegi  10048  xrpnfdc  10055  xrmnfdc  10056  xnegid  10072  xaddcom  10074  xaddid1  10075  xnegdi  10081  xleadd1a  10086  xltadd1  10089  xlt2add  10093  xsubge0  10094  xposdif  10095  xleaddadd  10100  qbtwnxr  10494  xrmaxiflemcl  11777  xrmaxifle  11778  xrmaxiflemab  11779  xrmaxiflemlub  11780  xrmaxltsup  11790  xrmaxadd  11793  xrbdtri  11808  isxmet2d  15043  blssioo  15248