Theorem elxr 10105

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 8308	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2299	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3359	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8323	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8326	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2825	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3710	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 770	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1008	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 187	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 206	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 105   ∨ wo 716   ∨ w3o 1004   = wceq 1398   ∈ wcel 2203   ∪ cun 3208  {cpr 3689  ℝcr 8122  +∞cpnf 8301  -∞cmnf 8302  ℝ^*cxr 8303

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-un 4553  ax-cnex 8214

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-uni 3914  df-pnf 8306  df-mnf 8307  df-xr 8308

This theorem is referenced by:  xrnemnf  10106  xrnepnf  10107  xrltnr  10108  xrltnsym  10122  xrlttr  10124  xrltso  10125  xrlttri3  10126  nltpnft  10143  npnflt  10144  ngtmnft  10146  nmnfgt  10147  xrrebnd  10148  xnegcl  10161  xnegneg  10162  xltnegi  10164  xrpnfdc  10171  xrmnfdc  10172  xnegid  10188  xaddcom  10190  xaddid1  10191  xnegdi  10197  xleadd1a  10202  xltadd1  10205  xlt2add  10209  xsubge0  10210  xposdif  10211  xleaddadd  10216  qbtwnxr  10613  xrmaxiflemcl  11923  xrmaxifle  11924  xrmaxiflemab  11925  xrmaxiflemlub  11926  xrmaxltsup  11936  xrmaxadd  11939  xrbdtri  11954  isxmet2d  15200  blssioo  15405