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

Theorem elxr 11377
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 9661 . . 3  |-  RR*  =  ( RR  u.  { +oo , -oo } )
21eleq2i 2480 . 2  |-  ( A  e.  RR*  <->  A  e.  ( RR  u.  { +oo , -oo } ) )
3 elun 3583 . 2  |-  ( A  e.  ( RR  u.  { +oo , -oo }
)  <->  ( A  e.  RR  \/  A  e. 
{ +oo , -oo }
) )
4 pnfex 11374 . . . . 5  |- +oo  e.  _V
5 mnfxr 11375 . . . . . 6  |- -oo  e.  RR*
65elexi 3068 . . . . 5  |- -oo  e.  _V
74, 6elpr2 3990 . . . 4  |-  ( A  e.  { +oo , -oo }  <->  ( A  = +oo  \/  A  = -oo ) )
87orbi2i 517 . . 3  |-  ( ( A  e.  RR  \/  A  e.  { +oo , -oo } )  <->  ( A  e.  RR  \/  ( A  = +oo  \/  A  = -oo ) ) )
9 3orass 977 . . 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 366    \/ w3o 973    = wceq 1405    e. wcel 1842    u. cun 3411   {cpr 3973   RRcr 9520   +oocpnf 9654   -oocmnf 9655   RR*cxr 9656
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-pow 4571  ax-un 6573  ax-cnex 9577
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2759  df-v 3060  df-un 3418  df-in 3420  df-ss 3427  df-pw 3956  df-sn 3972  df-pr 3974  df-uni 4191  df-pnf 9659  df-mnf 9660  df-xr 9661
This theorem is referenced by:  xrnemnf  11380  xrnepnf  11381  xrltnr  11382  xrltnsym  11395  xrlttri  11397  xrlttr  11398  xrrebnd  11421  qbtwnxr  11451  xnegcl  11464  xnegneg  11465  xltnegi  11467  xaddf  11475  xnegid  11487  xaddcom  11489  xaddid1  11490  xnegdi  11492  xleadd1a  11497  xlt2add  11504  xsubge0  11505  xmullem  11508  xmulid1  11523  xmulgt0  11527  xmulasslem3  11530  xlemul1a  11532  xadddilem  11538  xadddi2  11541  xrsupsslem  11550  xrinfmsslem  11551  xrub  11555  isxmet2d  21120  blssioo  21590  ioombl1  22262  ismbf2d  22338  itg2seq  22439  xaddeq0  28000  relowlssretop  31266  iccpartiltu  37670  iccpartigtl  37671
  Copyright terms: Public domain W3C validator