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

Theorem pnfex 10499
Description: Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.) (Revised by Steven Nguyen, 7-Dec-2022.)
Assertion
Ref Expression
pnfex +∞ ∈ V

Proof of Theorem pnfex
StepHypRef Expression
1 df-pnf 10482 . 2 +∞ = 𝒫
2 cnex 10422 . . . 4 ℂ ∈ V
32uniex 7289 . . 3 ℂ ∈ V
43pwex 5138 . 2 𝒫 ℂ ∈ V
51, 4eqeltri 2864 1 +∞ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2051  Vcvv 3417  𝒫 cpw 4425   cuni 4717  cc 10339  +∞cpnf 10477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752  ax-sep 5064  ax-pow 5123  ax-un 7285  ax-cnex 10397
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-rex 3096  df-v 3419  df-in 3838  df-ss 3845  df-pw 4427  df-uni 4718  df-pnf 10482
This theorem is referenced by:  pnfxr  10500  mnfxr  10504  elxnn0  11787  elxr  12334  xnegex  12424  xaddval  12439  xmulval  12441  xrinfmss  12525  hashgval  13514  hashinf  13516  hashfxnn0  13518  pcval  16043  pc0  16053  ramcl2  16214  iccpnfhmeo  23267  taylfval  24665  xrlimcnp  25263  xrge0iifcv  30853  xrge0iifiso  30854  xrge0iifhom  30856  sge0f1o  42130  sge0sup  42139  sge0pnfmpt  42193
  Copyright terms: Public domain W3C validator