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

Theorem elxr 10458
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 8871 . . 3  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
21eleq2i 2347 . 2  |-  ( A  e.  RR*  <->  A  e.  ( RR  u.  {  +oo ,  -oo } ) )
3 elun 3316 . 2  |-  ( A  e.  ( RR  u.  { 
+oo ,  -oo } )  <-> 
( A  e.  RR  \/  A  e.  {  +oo , 
-oo } ) )
4 pnfxr 10455 . . . . . 6  |-  +oo  e.  RR*
54elexi 2797 . . . . 5  |-  +oo  e.  _V
6 mnfxr 10456 . . . . . 6  |-  -oo  e.  RR*
76elexi 2797 . . . . 5  |-  -oo  e.  _V
85, 7elpr2 3659 . . . 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 1623    e. wcel 1684    u. cun 3150   {cpr 3641   RRcr 8736    +oocpnf 8864    -oocmnf 8865   RR*cxr 8866
This theorem is referenced by:  xrnemnf  10460  xrnepnf  10461  xrltnr  10462  xrltnsym  10471  xrlttri  10473  xrlttr  10474  xrrebnd  10497  qbtwnxr  10527  xnegcl  10540  xnegneg  10541  xltnegi  10543  xaddf  10551  xnegid  10563  xaddcom  10565  xaddid1  10566  xnegdi  10568  xleadd1a  10573  xlt2add  10580  xsubge0  10581  xmullem  10584  xmulid1  10599  xmulgt0  10603  xmulasslem3  10606  xlemul1a  10608  xadddilem  10614  xadddi2  10617  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  isxmet2d  17892  blssioo  18301  ioombl1  18919  ismbf2d  18996  itg2seq  19097  xaddeq0  23304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-pow 4188  ax-un 4512  ax-cnex 8793
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-pw 3627  df-sn 3646  df-pr 3647  df-uni 3828  df-pnf 8869  df-mnf 8870  df-xr 8871
  Copyright terms: Public domain W3C validator