MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pnfxr Structured version   Visualization version   GIF version

Theorem pnfxr 10077
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 +∞ ∈ ℝ*

Proof of Theorem pnfxr
StepHypRef Expression
1 ssun2 3769 . . 3 {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2 df-pnf 10061 . . . . 5 +∞ = 𝒫
3 cnex 10002 . . . . . . 7 ℂ ∈ V
43uniex 6938 . . . . . 6 ℂ ∈ V
54pwex 4839 . . . . 5 𝒫 ℂ ∈ V
62, 5eqeltri 2695 . . . 4 +∞ ∈ V
76prid1 4288 . . 3 +∞ ∈ {+∞, -∞}
81, 7sselii 3592 . 2 +∞ ∈ (ℝ ∪ {+∞, -∞})
9 df-xr 10063 . 2 * = (ℝ ∪ {+∞, -∞})
108, 9eleqtrri 2698 1 +∞ ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  Vcvv 3195  cun 3565  𝒫 cpw 4149  {cpr 4170   cuni 4427  cc 9919  cr 9920  +∞cpnf 10056  -∞cmnf 10057  *cxr 10058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-pow 4834  ax-un 6934  ax-cnex 9977
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-v 3197  df-un 3572  df-in 3574  df-ss 3581  df-pw 4151  df-sn 4169  df-pr 4171  df-uni 4428  df-pnf 10061  df-xr 10063
This theorem is referenced by:  pnfex  10078  pnfnemnf  10079  xnn0xr  11353  xrltnr  11938  ltpnf  11939  mnfltpnf  11945  pnfnlt  11947  pnfge  11949  nltpnft  11980  xgepnf  11981  xrre  11985  xrre2  11986  xnegcl  12029  xaddf  12040  xaddpnf1  12042  xaddpnf2  12043  pnfaddmnf  12046  mnfaddpnf  12047  xaddass2  12065  xlt2add  12075  xsubge0  12076  xmulneg1  12084  xmulf  12087  xmulpnf1  12089  xmulpnf2  12090  xmulmnf1  12091  xmulpnf1n  12093  xlemul1a  12103  xadddilem  12109  xadddi2  12112  xrsupsslem  12122  xrinfmsslem  12123  supxrpnf  12133  supxrunb1  12134  supxrunb2  12135  supxrbnd  12143  xrinf0  12153  elicore  12211  elioc2  12221  elico2  12222  elicc2  12223  ioomax  12233  iccmax  12234  ioopos  12235  elioopnf  12252  elicopnf  12254  unirnioo  12258  xrge0neqmnf  12261  elxrge0  12266  difreicc  12289  xnn0xrge0  12310  ioopnfsup  12646  icopnfsup  12647  xrsup  12650  hashbnd  13106  hashnnn0genn0  13114  hashxrcl  13131  hashdomi  13152  sgnpnf  13814  rexico  14074  limsupgre  14193  rlim3  14210  fprodge0  14705  fprodge1  14707  pcxcl  15546  pc2dvds  15564  pcadd  15574  ramxrcl  15702  ramubcl  15703  xrsnsgrp  19763  xrsdsreclblem  19773  rge0srg  19798  leordtvallem1  20995  leordtval2  20997  lecldbas  21004  pnfnei  21005  mnfnei  21006  xblpnfps  22181  xblpnf  22182  xblss2ps  22187  blssec  22221  blpnfctr  22222  nmoix  22514  icopnfcld  22552  iocmnfcld  22553  xrtgioo  22590  reconnlem1  22610  xrge0tsms  22618  metdstri  22635  iccpnfcnv  22724  ovolf  23231  ovolicopnf  23273  ovolre  23274  volsup  23305  ioombl1lem4  23310  icombl1  23312  icombl  23313  ioombl  23314  uniioombllem1  23330  mbfdm  23376  ismbfd  23388  mbfmax  23397  ismbf3d  23402  itg2ge0  23483  lhop2  23759  dvfsumlem2  23771  dvfsumrlim  23775  dvfsumrlim2  23776  taylfvallem1  24092  taylfval  24094  tayl0  24097  radcnvcl  24152  radcnvle  24155  psercnlem1  24160  logccv  24390  rlimcnp  24673  rlimcnp2  24674  xrlimcnp  24676  logfacbnd3  24929  chebbnd1  25142  chebbnd2  25147  dchrisumlem3  25161  log2sumbnd  25214  pntpbnd1  25256  pntibndlem2  25261  pntlemb  25267  pntleme  25278  pnt  25284  upgrfi  25967  topnfbey  27295  isblo3i  27626  xrge0infss  29499  dfrp2  29506  xrdifh  29516  elxrge02  29614  xdivpnfrp  29615  xrge0addass  29664  xrge0addgt0  29665  xrge0adddir  29666  xrge0npcan  29668  fsumrp0cl  29669  pnfinf  29711  xrnarchi  29712  xrge0tsmsd  29759  xrge0slmod  29818  unitssxrge0  29920  tpr2rico  29932  xrge0iifcnv  29953  xrge0iifiso  29955  xrge0iifhom  29957  xrge0mulc1cn  29961  pnfneige0  29971  lmxrge0  29972  esumle  30094  esumlef  30098  esumcst  30099  esumpr2  30103  esumpinfval  30109  esumpinfsum  30113  esumpcvgval  30114  hashf2  30120  esumcvg  30122  esumcvgsum  30124  voliune  30266  volfiniune  30267  ddemeas  30273  sxbrsigalem0  30307  sxbrsigalem2  30322  oms0  30333  sibfinima  30375  sitmcl  30387  probmeasb  30466  orvcgteel  30503  dstfrvclim1  30513  signsply0  30602  chtvalz  30681  hgt750lemf  30705  iooelexlt  33181  mbfposadd  33428  itg2addnclem2  33433  ftc1anclem5  33460  asindmre  33466  dvasin  33467  dvacos  33468  dvconstbi  38353  rfcnpre3  39012  absfico  39226  xadd0ge  39349  xrgepnfd  39360  xrge0nemnfd  39361  supxrgere  39362  supxrgelem  39366  supxrge  39367  xralrple2  39383  infxr  39396  infleinflem2  39400  xrralrecnnge  39426  infxrpnf  39487  iocopn  39549  pnfel0pnf  39557  ge0nemnf2  39558  ge0xrre  39561  ge0lere  39562  ressiooinf  39587  uzinico  39590  uzubioo  39597  fsumge0cl  39605  limcicciooub  39669  limsupre  39673  limcresiooub  39674  limcleqr  39676  limsupresre  39728  limsupresico  39732  limsuppnfdlem  39733  limsuppnflem  39742  limsupmnflem  39752  liminfresico  39797  limsup10exlem  39798  liminflelimsuplem  39801  liminflelimsupuz  39811  icccncfext  39863  iblsplit  39945  itgsubsticclem  39954  fourierdlem31  40118  fourierdlem33  40120  fourierdlem46  40132  fourierdlem47  40133  fourierdlem48  40134  fourierdlem49  40135  fourierdlem65  40151  fourierdlem73  40159  fourierdlem75  40161  fourierdlem85  40171  fourierdlem88  40174  fourierdlem95  40181  fourierdlem97  40183  fourierdlem103  40189  fourierdlem104  40190  fourierdlem107  40193  fourierdlem109  40195  fourierdlem111  40197  fourierdlem112  40198  fourierdlem113  40199  fouriersw  40211  ioorrnopnxrlem  40289  sge0val  40346  fge0iccico  40350  gsumge0cl  40351  sge0sn  40359  sge0tsms  40360  sge0cl  40361  sge0f1o  40362  sge0ge0  40364  sge0repnf  40366  sge0fsum  40367  sge0pr  40374  sge0prle  40381  sge0split  40389  sge0p1  40394  sge0iunmptlemre  40395  sge0rpcpnf  40401  sge0rernmpt  40402  sge0isum  40407  sge0ad2en  40411  sge0xaddlem1  40413  sge0xaddlem2  40414  sge0uzfsumgt  40424  sge0seq  40426  sge0reuz  40427  voliunsge0lem  40452  meage0  40455  meassre  40457  meaiuninclem  40460  omessre  40487  omeiunltfirp  40496  carageniuncllem2  40499  carageniuncl  40500  omege0  40510  hoiprodcl  40524  hoicvrrex  40533  ovnpnfelsup  40536  ovnlerp  40539  ovnf  40540  ovn0lem  40542  ovnsubaddlem1  40547  hoiprodcl3  40557  hoidmvcl  40559  sge0hsphoire  40566  hoidmv1lelem1  40568  hoidmv1lelem2  40569  hoidmv1lelem3  40570  hoidmv1le  40571  hoidmvlelem1  40572  hoidmvlelem4  40575  hoidmvlelem5  40576  ovnhoilem1  40578  volicorege0  40614  ovolval5lem1  40629  pimgtpnf2  40680  pimiooltgt  40684  smfliminflem  40799
  Copyright terms: Public domain W3C validator