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

Theorem elxr 13159
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 11300 . . 3 * = (ℝ ∪ {+∞, -∞})
21eleq2i 2832 . 2 (𝐴 ∈ ℝ*𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3 elun 4152 . 2 (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4 pnfex 11315 . . . . 5 +∞ ∈ V
5 mnfxr 11319 . . . . . 6 -∞ ∈ ℝ*
65elexi 3502 . . . . 5 -∞ ∈ V
74, 6elpr2 4651 . . . 4 (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
87orbi2i 912 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9 3orass 1089 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
108, 9bitr4i 278 . 2 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
112, 3, 103bitri 297 1 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wo 847  w3o 1085   = wceq 1539  wcel 2107  cun 3948  {cpr 4627  cr 11155  +∞cpnf 11293  -∞cmnf 11294  *cxr 11295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-pow 5364  ax-un 7756  ax-cnex 11212
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-ss 3967  df-pw 4601  df-sn 4626  df-pr 4628  df-uni 4907  df-pnf 11298  df-mnf 11299  df-xr 11300
This theorem is referenced by:  xrnemnf  13160  xrnepnf  13161  xrltnr  13162  xrltnsym  13180  xrlttri  13182  xrlttr  13183  xrrebnd  13211  qbtwnxr  13243  xnegcl  13256  xnegneg  13257  xltnegi  13259  xaddf  13267  xnegid  13281  xaddcom  13283  xaddrid  13284  xnegdi  13291  xleadd1a  13296  xlt2add  13303  xsubge0  13304  xmullem  13307  xmulrid  13322  xmulgt0  13326  xmulasslem3  13329  xlemul1a  13331  xadddilem  13337  xadddi2  13340  xrsupsslem  13350  xrinfmsslem  13351  xrub  13355  reltxrnmnf  13385  isxmet2d  24338  blssioo  24817  ioombl1  25598  ismbf2d  25676  itg2seq  25778  xaddeq0  32758  iooelexlt  37364  relowlssretop  37365  iccpartiltu  47414  iccpartigtl  47415
  Copyright terms: Public domain W3C validator