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

Theorem pnfex 11314
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 11297 . 2 +∞ = 𝒫
2 cnex 11236 . . . 4 ℂ ∈ V
32uniex 7761 . . 3 ℂ ∈ V
43pwex 5380 . 2 𝒫 ℂ ∈ V
51, 4eqeltri 2837 1 +∞ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  Vcvv 3480  𝒫 cpw 4600   cuni 4907  cc 11153  +∞cpnf 11292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pow 5365  ax-un 7755  ax-cnex 11211
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602  df-uni 4908  df-pnf 11297
This theorem is referenced by:  pnfxr  11315  mnfxr  11318  elxnn0  12601  elxr  13158  xnegex  13250  xaddval  13265  xmulval  13267  xrinfmss  13352  hashgval  14372  hashinf  14374  hashfxnn0  14376  pcval  16882  pc0  16892  ramcl2  17054  iccpnfhmeo  24976  taylfval  26400  xrlimcnp  27011  xrge0iifcv  33933  xrge0iifiso  33934  xrge0iifhom  33936  sge0f1o  46397  sge0sup  46406  sge0pnfmpt  46460
  Copyright terms: Public domain W3C validator