Theorem pnfex 11234

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

Step	Hyp	Ref	Expression
1		df-pnf 11217	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11156	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7720	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5338	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2825	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450  𝒫 cpw 4566  ∪ cuni 4874  ℂcc 11073  +∞cpnf 11212

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-pow 5323  ax-un 7714  ax-cnex 11131

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568  df-uni 4875  df-pnf 11217

This theorem is referenced by:  pnfxr  11235  mnfxr  11238  elxnn0  12524  elxr  13083  xnegex  13175  xaddval  13190  xmulval  13192  xrinfmss  13277  hashgval  14305  hashinf  14307  hashfxnn0  14309  pcval  16822  pc0  16832  ramcl2  16994  iccpnfhmeo  24850  taylfval  26273  xrlimcnp  26885  xrge0iifcv  33931  xrge0iifiso  33932  xrge0iifhom  33934  sge0f1o  46387  sge0sup  46396  sge0pnfmpt  46450