Theorem pnfex 11168

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 11151	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11090	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7677	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5319	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2824	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3436  𝒫 cpw 4551  ∪ cuni 4858  ℂcc 11007  +∞cpnf 11146

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 2701  ax-sep 5235  ax-pow 5304  ax-un 7671  ax-cnex 11065

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-pw 4553  df-uni 4859  df-pnf 11151

This theorem is referenced by:  pnfxr  11169  mnfxr  11172  elxnn0  12459  elxr  13018  xnegex  13110  xaddval  13125  xmulval  13127  xrinfmss  13212  hashgval  14240  hashinf  14242  hashfxnn0  14244  pcval  16756  pc0  16766  ramcl2  16928  iccpnfhmeo  24841  taylfval  26264  xrlimcnp  26876  xrge0iifcv  33901  xrge0iifiso  33902  xrge0iifhom  33904  sge0f1o  46367  sge0sup  46376  sge0pnfmpt  46430