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

Theorem pnfex 11207
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 11190 . 2 +∞ = 𝒫
2 cnex 11131 . . . 4 ℂ ∈ V
32uniex 7677 . . 3 ℂ ∈ V
43pwex 5335 . 2 𝒫 ℂ ∈ V
51, 4eqeltri 2834 1 +∞ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3445  𝒫 cpw 4560   cuni 4865  cc 11048  +∞cpnf 11185
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-pow 5320  ax-un 7671  ax-cnex 11106
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927  df-pw 4562  df-uni 4866  df-pnf 11190
This theorem is referenced by:  pnfxr  11208  mnfxr  11211  elxnn0  12486  elxr  13036  xnegex  13126  xaddval  13141  xmulval  13143  xrinfmss  13228  hashgval  14232  hashinf  14234  hashfxnn0  14236  pcval  16715  pc0  16725  ramcl2  16887  iccpnfhmeo  24306  taylfval  25716  xrlimcnp  26316  xrge0iifcv  32506  xrge0iifiso  32507  xrge0iifhom  32509  sge0f1o  44595  sge0sup  44604  sge0pnfmpt  44658
  Copyright terms: Public domain W3C validator