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

Theorem elxr 13131
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 11284 . . 3 * = (ℝ ∪ {+∞, -∞})
21eleq2i 2817 . 2 (𝐴 ∈ ℝ*𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3 elun 4145 . 2 (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4 pnfex 11299 . . . . 5 +∞ ∈ V
5 mnfxr 11303 . . . . . 6 -∞ ∈ ℝ*
65elexi 3482 . . . . 5 -∞ ∈ V
74, 6elpr2 4656 . . . 4 (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
87orbi2i 910 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9 3orass 1087 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
108, 9bitr4i 277 . 2 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
112, 3, 103bitri 296 1 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wo 845  w3o 1083   = wceq 1533  wcel 2098  cun 3942  {cpr 4632  cr 11139  +∞cpnf 11277  -∞cmnf 11278  *cxr 11279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-pow 5365  ax-un 7741  ax-cnex 11196
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-ss 3961  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4910  df-pnf 11282  df-mnf 11283  df-xr 11284
This theorem is referenced by:  xrnemnf  13132  xrnepnf  13133  xrltnr  13134  xrltnsym  13151  xrlttri  13153  xrlttr  13154  xrrebnd  13182  qbtwnxr  13214  xnegcl  13227  xnegneg  13228  xltnegi  13230  xaddf  13238  xnegid  13252  xaddcom  13254  xaddrid  13255  xnegdi  13262  xleadd1a  13267  xlt2add  13274  xsubge0  13275  xmullem  13278  xmulrid  13293  xmulgt0  13297  xmulasslem3  13300  xlemul1a  13302  xadddilem  13308  xadddi2  13311  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  reltxrnmnf  13356  isxmet2d  24277  blssioo  24755  ioombl1  25535  ismbf2d  25613  itg2seq  25716  xaddeq0  32605  iooelexlt  36972  relowlssretop  36973  iccpartiltu  46899  iccpartigtl  46900
  Copyright terms: Public domain W3C validator