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

Theorem pnfex 11196
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 11195 . 2  |- +oo  e.  RR*
21elexi 3080 1  |- +oo  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   _Vcvv 3070   +oocpnf 9518   RR*cxr 9520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-pow 4570  ax-un 6474  ax-cnex 9441
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-v 3072  df-un 3433  df-in 3435  df-ss 3442  df-pw 3962  df-sn 3978  df-pr 3980  df-uni 4192  df-pnf 9523  df-xr 9525
This theorem is referenced by:  mnfxr  11197  elxr  11199  xnegex  11281  xaddval  11296  xmulval  11298  xrinfmss  11375  xrinfm0  11402  hashgval  12209  hashinf  12211  hashf  12213  pcval  14015  pc0  14025  ramcl2  14181  iccpnfhmeo  20635  taylfval  21942  xrlimcnp  22480  vdgrf  23705  xrge0iifcv  26500  xrge0iifiso  26501  xrge0iifhom  26503
  Copyright terms: Public domain W3C validator