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

Theorem pnfxr 7285
Description: Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
Assertion
Ref Expression
pnfxr  |- +oo  e.  RR*

Proof of Theorem pnfxr
StepHypRef Expression
1 ssun2 3146 . . 3  |-  { +oo , -oo }  C_  ( RR  u.  { +oo , -oo } )
2 df-pnf 7269 . . . . 5  |- +oo  =  ~P U. CC
3 cnex 7211 . . . . . . 7  |-  CC  e.  _V
43uniex 4220 . . . . . 6  |-  U. CC  e.  _V
54pwex 3973 . . . . 5  |-  ~P U. CC  e.  _V
62, 5eqeltri 2155 . . . 4  |- +oo  e.  _V
76prid1 3516 . . 3  |- +oo  e.  { +oo , -oo }
81, 7sselii 3005 . 2  |- +oo  e.  ( RR  u.  { +oo , -oo } )
9 df-xr 7271 . 2  |-  RR*  =  ( RR  u.  { +oo , -oo } )
108, 9eleqtrri 2158 1  |- +oo  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1434   _Vcvv 2610    u. cun 2980   ~Pcpw 3400   {cpr 3417   U.cuni 3621   CCcc 7093   RRcr 7094   +oocpnf 7264   -oocmnf 7265   RR*cxr 7266
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-un 4216  ax-cnex 7181
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2612  df-un 2986  df-in 2988  df-ss 2995  df-pw 3402  df-sn 3422  df-pr 3423  df-uni 3622  df-pnf 7269  df-xr 7271
This theorem is referenced by:  pnfex  7286  pnfnemnf  7287  xnn0xr  8475  xrltnr  8983  ltpnf  8984  mnfltpnf  8988  pnfnlt  8990  pnfge  8992  xrlttri3  9000  nltpnft  9012  xrrebnd  9014  xrre  9015  xrre2  9016  xnegcl  9027  xrex  9038  elioc2  9087  elico2  9088  elicc2  9089  ioomax  9099  iccmax  9100  ioopos  9101  elioopnf  9118  elicopnf  9120  unirnioo  9124  elxrge0  9129  hashinfom  9854  rexico  10308
  Copyright terms: Public domain W3C validator