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

Theorem elxr 12163
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 10290 . . 3 * = (ℝ ∪ {+∞, -∞})
21eleq2i 2831 . 2 (𝐴 ∈ ℝ*𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3 elun 3896 . 2 (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4 pnfex 10305 . . . . 5 +∞ ∈ V
5 mnfxr 10308 . . . . . 6 -∞ ∈ ℝ*
65elexi 3353 . . . . 5 -∞ ∈ V
74, 6elpr2 4344 . . . 4 (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
87orbi2i 542 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9 3orass 1075 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
108, 9bitr4i 267 . 2 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
112, 3, 103bitri 286 1 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382  w3o 1071   = wceq 1632  wcel 2139  cun 3713  {cpr 4323  cr 10147  +∞cpnf 10283  -∞cmnf 10284  *cxr 10285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-pow 4992  ax-un 7115  ax-cnex 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-v 3342  df-un 3720  df-in 3722  df-ss 3729  df-pw 4304  df-sn 4322  df-pr 4324  df-uni 4589  df-pnf 10288  df-mnf 10289  df-xr 10290
This theorem is referenced by:  xrnemnf  12164  xrnepnf  12165  xrltnr  12166  xrltnsym  12183  xrlttri  12185  xrlttr  12186  xrrebnd  12212  qbtwnxr  12244  xnegcl  12257  xnegneg  12258  xltnegi  12260  xaddf  12268  xnegid  12282  xaddcom  12284  xaddid1  12285  xnegdi  12291  xleadd1a  12296  xlt2add  12303  xsubge0  12304  xmullem  12307  xmulid1  12322  xmulgt0  12326  xmulasslem3  12329  xlemul1a  12331  xadddilem  12337  xadddi2  12340  xrsupsslem  12350  xrinfmsslem  12351  xrub  12355  reltxrnmnf  12385  isxmet2d  22353  blssioo  22819  ioombl1  23550  ismbf2d  23627  itg2seq  23728  xaddeq0  29848  iooelexlt  33539  relowlssretop  33540  iccpartiltu  41886  iccpartigtl  41887
  Copyright terms: Public domain W3C validator