Theorem elxr 9905

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 8118	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2273	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3315	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8133	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8136	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2785	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3656	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 764	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 984	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 187	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 206	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 105   ∨ wo 710   ∨ w3o 980   = wceq 1373   ∈ wcel 2177   ∪ cun 3165  {cpr 3635  ℝcr 7931  +∞cpnf 8111  -∞cmnf 8112  ℝ^*cxr 8113

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-un 4484  ax-cnex 8023

This theorem depends on definitions:  df-bi 117  df-3or 982  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-uni 3853  df-pnf 8116  df-mnf 8117  df-xr 8118

This theorem is referenced by:  xrnemnf  9906  xrnepnf  9907  xrltnr  9908  xrltnsym  9922  xrlttr  9924  xrltso  9925  xrlttri3  9926  nltpnft  9943  npnflt  9944  ngtmnft  9946  nmnfgt  9947  xrrebnd  9948  xnegcl  9961  xnegneg  9962  xltnegi  9964  xrpnfdc  9971  xrmnfdc  9972  xnegid  9988  xaddcom  9990  xaddid1  9991  xnegdi  9997  xleadd1a  10002  xltadd1  10005  xlt2add  10009  xsubge0  10010  xposdif  10011  xleaddadd  10016  qbtwnxr  10407  xrmaxiflemcl  11600  xrmaxifle  11601  xrmaxiflemab  11602  xrmaxiflemlub  11603  xrmaxltsup  11613  xrmaxadd  11616  xrbdtri  11631  isxmet2d  14864  blssioo  15069