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

Theorem pnfex 10683
 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 10666 . 2 +∞ = 𝒫
2 cnex 10607 . . . 4 ℂ ∈ V
32uniex 7447 . . 3 ℂ ∈ V
43pwex 5246 . 2 𝒫 ℂ ∈ V
51, 4eqeltri 2886 1 +∞ ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2111  Vcvv 3441  𝒫 cpw 4497  ∪ cuni 4800  ℂcc 10524  +∞cpnf 10661 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-pow 5231  ax-un 7441  ax-cnex 10582 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499  df-uni 4801  df-pnf 10666 This theorem is referenced by:  pnfxr  10684  mnfxr  10687  elxnn0  11957  elxr  12499  xnegex  12589  xaddval  12604  xmulval  12606  xrinfmss  12691  hashgval  13689  hashinf  13691  hashfxnn0  13693  pcval  16171  pc0  16181  ramcl2  16342  iccpnfhmeo  23550  taylfval  24954  xrlimcnp  25554  xrge0iifcv  31287  xrge0iifiso  31288  xrge0iifhom  31290  sge0f1o  43016  sge0sup  43025  sge0pnfmpt  43079
 Copyright terms: Public domain W3C validator