ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elxr Unicode version

Theorem elxr 9450
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 7722 . . 3  |-  RR*  =  ( RR  u.  { +oo , -oo } )
21eleq2i 2179 . 2  |-  ( A  e.  RR*  <->  A  e.  ( RR  u.  { +oo , -oo } ) )
3 elun 3181 . 2  |-  ( A  e.  ( RR  u.  { +oo , -oo }
)  <->  ( A  e.  RR  \/  A  e. 
{ +oo , -oo }
) )
4 pnfex 7737 . . . . 5  |- +oo  e.  _V
5 mnfxr 7740 . . . . . 6  |- -oo  e.  RR*
65elexi 2667 . . . . 5  |- -oo  e.  _V
74, 6elpr2 3513 . . . 4  |-  ( A  e.  { +oo , -oo }  <->  ( A  = +oo  \/  A  = -oo ) )
87orbi2i 734 . . 3  |-  ( ( A  e.  RR  \/  A  e.  { +oo , -oo } )  <->  ( A  e.  RR  \/  ( A  = +oo  \/  A  = -oo ) ) )
9 3orass 946 . . 3  |-  ( ( A  e.  RR  \/  A  = +oo  \/  A  = -oo )  <->  ( A  e.  RR  \/  ( A  = +oo  \/  A  = -oo ) ) )
108, 9bitr4i 186 . 2  |-  ( ( A  e.  RR  \/  A  e.  { +oo , -oo } )  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
112, 3, 103bitri 205 1  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 680    \/ w3o 942    = wceq 1312    e. wcel 1461    u. cun 3033   {cpr 3492   RRcr 7540   +oocpnf 7715   -oocmnf 7716   RR*cxr 7717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-un 4313  ax-cnex 7630
This theorem depends on definitions:  df-bi 116  df-3or 944  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-uni 3701  df-pnf 7720  df-mnf 7721  df-xr 7722
This theorem is referenced by:  xrnemnf  9451  xrnepnf  9452  xrltnr  9453  xrltnsym  9466  xrlttr  9468  xrltso  9469  xrlttri3  9470  nltpnft  9484  npnflt  9485  ngtmnft  9487  nmnfgt  9488  xrrebnd  9489  xnegcl  9502  xnegneg  9503  xltnegi  9505  xrpnfdc  9512  xrmnfdc  9513  xnegid  9529  xaddcom  9531  xaddid1  9532  xnegdi  9538  xleadd1a  9543  xltadd1  9546  xlt2add  9550  xsubge0  9551  xposdif  9552  xleaddadd  9557  qbtwnxr  9922  xrmaxiflemcl  10900  xrmaxifle  10901  xrmaxiflemab  10902  xrmaxiflemlub  10903  xrmaxltsup  10913  xrmaxadd  10916  xrbdtri  10931  isxmet2d  12331  blssioo  12525
  Copyright terms: Public domain W3C validator