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

Theorem elxr 10474
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 8887 . . 3  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
21eleq2i 2360 . 2  |-  ( A  e.  RR*  <->  A  e.  ( RR  u.  {  +oo ,  -oo } ) )
3 elun 3329 . 2  |-  ( A  e.  ( RR  u.  { 
+oo ,  -oo } )  <-> 
( A  e.  RR  \/  A  e.  {  +oo , 
-oo } ) )
4 pnfxr 10471 . . . . . 6  |-  +oo  e.  RR*
54elexi 2810 . . . . 5  |-  +oo  e.  _V
6 mnfxr 10472 . . . . . 6  |-  -oo  e.  RR*
76elexi 2810 . . . . 5  |-  -oo  e.  _V
85, 7elpr2 3672 . . . 4  |-  ( A  e.  {  +oo ,  -oo }  <->  ( A  = 
+oo  \/  A  =  -oo ) )
98orbi2i 505 . . 3  |-  ( ( A  e.  RR  \/  A  e.  {  +oo ,  -oo } )  <->  ( A  e.  RR  \/  ( A  =  +oo  \/  A  =  -oo ) ) )
10 3orass 937 . . 3  |-  ( ( A  e.  RR  \/  A  =  +oo  \/  A  =  -oo )  <->  ( A  e.  RR  \/  ( A  =  +oo  \/  A  =  -oo ) ) )
119, 10bitr4i 243 . 2  |-  ( ( A  e.  RR  \/  A  e.  {  +oo ,  -oo } )  <->  ( A  e.  RR  \/  A  = 
+oo  \/  A  =  -oo ) )
122, 3, 113bitri 262 1  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = 
+oo  \/  A  =  -oo ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    \/ w3o 933    = wceq 1632    e. wcel 1696    u. cun 3163   {cpr 3654   RRcr 8752    +oocpnf 8880    -oocmnf 8881   RR*cxr 8882
This theorem is referenced by:  xrnemnf  10476  xrnepnf  10477  xrltnr  10478  xrltnsym  10487  xrlttri  10489  xrlttr  10490  xrrebnd  10513  qbtwnxr  10543  xnegcl  10556  xnegneg  10557  xltnegi  10559  xaddf  10567  xnegid  10579  xaddcom  10581  xaddid1  10582  xnegdi  10584  xleadd1a  10589  xlt2add  10596  xsubge0  10597  xmullem  10600  xmulid1  10615  xmulgt0  10619  xmulasslem3  10622  xlemul1a  10624  xadddilem  10630  xadddi2  10633  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  isxmet2d  17908  blssioo  18317  ioombl1  18935  ismbf2d  19012  itg2seq  19113  xaddeq0  23319
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-pow 4204  ax-un 4528  ax-cnex 8809
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-pw 3640  df-sn 3659  df-pr 3660  df-uni 3844  df-pnf 8885  df-mnf 8886  df-xr 8887
  Copyright terms: Public domain W3C validator