MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elxr Structured version   Visualization version   GIF version

Theorem elxr 12261
Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
elxr (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Proof of Theorem elxr
StepHypRef Expression
1 df-xr 10415 . . 3 * = (ℝ ∪ {+∞, -∞})
21eleq2i 2851 . 2 (𝐴 ∈ ℝ*𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3 elun 3976 . 2 (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4 pnfex 10429 . . . . 5 +∞ ∈ V
5 mnfxr 10434 . . . . . 6 -∞ ∈ ℝ*
65elexi 3415 . . . . 5 -∞ ∈ V
74, 6elpr2 4422 . . . 4 (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
87orbi2i 899 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9 3orass 1074 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
108, 9bitr4i 270 . 2 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
112, 3, 103bitri 289 1 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wo 836  w3o 1070   = wceq 1601  wcel 2107  cun 3790  {cpr 4400  cr 10271  +∞cpnf 10408  -∞cmnf 10409  *cxr 10410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754  ax-sep 5017  ax-pow 5077  ax-un 7226  ax-cnex 10328
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-v 3400  df-un 3797  df-in 3799  df-ss 3806  df-pw 4381  df-sn 4399  df-pr 4401  df-uni 4672  df-pnf 10413  df-mnf 10414  df-xr 10415
This theorem is referenced by:  xrnemnf  12262  xrnepnf  12263  xrltnr  12264  xrltnsym  12280  xrlttri  12282  xrlttr  12283  xrrebnd  12311  qbtwnxr  12343  xnegcl  12356  xnegneg  12357  xltnegi  12359  xaddf  12367  xnegid  12381  xaddcom  12383  xaddid1  12384  xnegdi  12390  xleadd1a  12395  xlt2add  12402  xsubge0  12403  xmullem  12406  xmulid1  12421  xmulgt0  12425  xmulasslem3  12428  xlemul1a  12430  xadddilem  12436  xadddi2  12439  xrsupsslem  12449  xrinfmsslem  12450  xrub  12454  reltxrnmnf  12484  isxmet2d  22540  blssioo  23006  ioombl1  23766  ismbf2d  23844  itg2seq  23946  xaddeq0  30083  iooelexlt  33805  relowlssretop  33806  iccpartiltu  42390  iccpartigtl  42391
  Copyright terms: Public domain W3C validator