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

Theorem elxr 11321
Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
elxr  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )

Proof of Theorem elxr
StepHypRef Expression
1 df-xr 9628 . . 3  |-  RR*  =  ( RR  u.  { +oo , -oo } )
21eleq2i 2545 . 2  |-  ( A  e.  RR*  <->  A  e.  ( RR  u.  { +oo , -oo } ) )
3 elun 3645 . 2  |-  ( A  e.  ( RR  u.  { +oo , -oo }
)  <->  ( A  e.  RR  \/  A  e. 
{ +oo , -oo }
) )
4 pnfex 11318 . . . . 5  |- +oo  e.  _V
5 mnfxr 11319 . . . . . 6  |- -oo  e.  RR*
65elexi 3123 . . . . 5  |- -oo  e.  _V
74, 6elpr2 4046 . . . 4  |-  ( A  e.  { +oo , -oo }  <->  ( A  = +oo  \/  A  = -oo ) )
87orbi2i 519 . . 3  |-  ( ( A  e.  RR  \/  A  e.  { +oo , -oo } )  <->  ( A  e.  RR  \/  ( A  = +oo  \/  A  = -oo ) ) )
9 3orass 976 . . 3  |-  ( ( A  e.  RR  \/  A  = +oo  \/  A  = -oo )  <->  ( A  e.  RR  \/  ( A  = +oo  \/  A  = -oo ) ) )
108, 9bitr4i 252 . 2  |-  ( ( A  e.  RR  \/  A  e.  { +oo , -oo } )  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
112, 3, 103bitri 271 1  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    \/ w3o 972    = wceq 1379    e. wcel 1767    u. cun 3474   {cpr 4029   RRcr 9487   +oocpnf 9621   -oocmnf 9622   RR*cxr 9623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-pow 4625  ax-un 6574  ax-cnex 9544
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-pw 4012  df-sn 4028  df-pr 4030  df-uni 4246  df-pnf 9626  df-mnf 9627  df-xr 9628
This theorem is referenced by:  xrnemnf  11324  xrnepnf  11325  xrltnr  11326  xrltnsym  11339  xrlttri  11341  xrlttr  11342  xrrebnd  11365  qbtwnxr  11395  xnegcl  11408  xnegneg  11409  xltnegi  11411  xaddf  11419  xnegid  11431  xaddcom  11433  xaddid1  11434  xnegdi  11436  xleadd1a  11441  xlt2add  11448  xsubge0  11449  xmullem  11452  xmulid1  11467  xmulgt0  11471  xmulasslem3  11474  xlemul1a  11476  xadddilem  11482  xadddi2  11485  xrsupsslem  11494  xrinfmsslem  11495  xrub  11499  isxmet2d  20562  blssioo  21032  ioombl1  21704  ismbf2d  21780  itg2seq  21881  xaddeq0  27238
  Copyright terms: Public domain W3C validator