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

Theorem pnfex 11265
Description: Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
pnfex  |- +oo  e.  _V

Proof of Theorem pnfex
StepHypRef Expression
1 pnfxr 11264 . 2  |- +oo  e.  RR*
21elexi 3061 1  |- +oo  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1836   _Vcvv 3051   +oocpnf 9558   RR*cxr 9560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-pow 4560  ax-un 6513  ax-cnex 9481
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-rex 2752  df-v 3053  df-un 3411  df-in 3413  df-ss 3420  df-pw 3946  df-sn 3962  df-pr 3964  df-uni 4181  df-pnf 9563  df-xr 9565
This theorem is referenced by:  mnfxr  11266  elxr  11268  xnegex  11350  xaddval  11365  xmulval  11367  xrinfmss  11444  xrinfm0  11471  hashgval  12333  hashinf  12335  hashf  12337  pcval  14393  pc0  14403  ramcl2  14559  iccpnfhmeo  21553  taylfval  22862  xrlimcnp  23438  vdgrf  25044  xrge0iifcv  28105  xrge0iifiso  28106  xrge0iifhom  28108
  Copyright terms: Public domain W3C validator