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

Theorem pnfex 10375
Description: Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
pnfex +∞ ∈ V

Proof of Theorem pnfex
StepHypRef Expression
1 pnfxr 10374 . 2 +∞ ∈ ℝ*
21elexi 3406 1 +∞ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2158  Vcvv 3390  +∞cpnf 10353  *cxr 10355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-pow 5032  ax-un 7176  ax-cnex 10274
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rex 3101  df-v 3392  df-un 3771  df-in 3773  df-ss 3780  df-pw 4350  df-sn 4368  df-pr 4370  df-uni 4627  df-pnf 10358  df-xr 10360
This theorem is referenced by:  mnfxr  10378  elxnn0  11627  elxr  12162  xnegex  12253  xaddval  12268  xmulval  12270  xrinfmss  12354  hashgval  13336  hashinf  13338  hashfxnn0  13340  hashfOLD  13342  pcval  15762  pc0  15772  ramcl2  15933  iccpnfhmeo  22953  taylfval  24323  xrlimcnp  24905  xrge0iifcv  30302  xrge0iifiso  30303  xrge0iifhom  30305  sge0f1o  41075  sge0sup  41084  sge0pnfmpt  41138
  Copyright terms: Public domain W3C validator