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

Theorem elxr 11350
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 9649 . . 3  |-  RR*  =  ( RR  u.  { +oo , -oo } )
21eleq2i 2535 . 2  |-  ( A  e.  RR*  <->  A  e.  ( RR  u.  { +oo , -oo } ) )
3 elun 3641 . 2  |-  ( A  e.  ( RR  u.  { +oo , -oo }
)  <->  ( A  e.  RR  \/  A  e. 
{ +oo , -oo }
) )
4 pnfex 11347 . . . . 5  |- +oo  e.  _V
5 mnfxr 11348 . . . . . 6  |- -oo  e.  RR*
65elexi 3119 . . . . 5  |- -oo  e.  _V
74, 6elpr2 4051 . . . 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 1395    e. wcel 1819    u. cun 3469   {cpr 4034   RRcr 9508   +oocpnf 9642   -oocmnf 9643   RR*cxr 9644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-pow 4634  ax-un 6591  ax-cnex 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-un 3476  df-in 3478  df-ss 3485  df-pw 4017  df-sn 4033  df-pr 4035  df-uni 4252  df-pnf 9647  df-mnf 9648  df-xr 9649
This theorem is referenced by:  xrnemnf  11353  xrnepnf  11354  xrltnr  11355  xrltnsym  11368  xrlttri  11370  xrlttr  11371  xrrebnd  11394  qbtwnxr  11424  xnegcl  11437  xnegneg  11438  xltnegi  11440  xaddf  11448  xnegid  11460  xaddcom  11462  xaddid1  11463  xnegdi  11465  xleadd1a  11470  xlt2add  11477  xsubge0  11478  xmullem  11481  xmulid1  11496  xmulgt0  11500  xmulasslem3  11503  xlemul1a  11505  xadddilem  11511  xadddi2  11514  xrsupsslem  11523  xrinfmsslem  11524  xrub  11528  isxmet2d  20955  blssioo  21425  ioombl1  22097  ismbf2d  22173  itg2seq  22274  xaddeq0  27723
  Copyright terms: Public domain W3C validator