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

Theorem elxr 11208
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 9534 . . 3  |-  RR*  =  ( RR  u.  { +oo , -oo } )
21eleq2i 2532 . 2  |-  ( A  e.  RR*  <->  A  e.  ( RR  u.  { +oo , -oo } ) )
3 elun 3606 . 2  |-  ( A  e.  ( RR  u.  { +oo , -oo }
)  <->  ( A  e.  RR  \/  A  e. 
{ +oo , -oo }
) )
4 pnfex 11205 . . . . 5  |- +oo  e.  _V
5 mnfxr 11206 . . . . . 6  |- -oo  e.  RR*
65elexi 3088 . . . . 5  |- -oo  e.  _V
74, 6elpr2 4005 . . . 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 968 . . 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 964    = wceq 1370    e. wcel 1758    u. cun 3435   {cpr 3988   RRcr 9393   +oocpnf 9527   -oocmnf 9528   RR*cxr 9529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-pow 4579  ax-un 6483  ax-cnex 9450
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2805  df-v 3080  df-un 3442  df-in 3444  df-ss 3451  df-pw 3971  df-sn 3987  df-pr 3989  df-uni 4201  df-pnf 9532  df-mnf 9533  df-xr 9534
This theorem is referenced by:  xrnemnf  11211  xrnepnf  11212  xrltnr  11213  xrltnsym  11226  xrlttri  11228  xrlttr  11229  xrrebnd  11252  qbtwnxr  11282  xnegcl  11295  xnegneg  11296  xltnegi  11298  xaddf  11306  xnegid  11318  xaddcom  11320  xaddid1  11321  xnegdi  11323  xleadd1a  11328  xlt2add  11335  xsubge0  11336  xmullem  11339  xmulid1  11354  xmulgt0  11358  xmulasslem3  11361  xlemul1a  11363  xadddilem  11369  xadddi2  11372  xrsupsslem  11381  xrinfmsslem  11382  xrub  11386  isxmet2d  20035  blssioo  20505  ioombl1  21177  ismbf2d  21253  itg2seq  21354  xaddeq0  26198
  Copyright terms: Public domain W3C validator