Theorem pnfex 10959

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 10942	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 10883	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7572	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5298	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2835	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422  𝒫 cpw 4530  ∪ cuni 4836  ℂcc 10800  +∞cpnf 10937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-pow 5283  ax-un 7566  ax-cnex 10858

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532  df-uni 4837  df-pnf 10942

This theorem is referenced by:  pnfxr  10960  mnfxr  10963  elxnn0  12237  elxr  12781  xnegex  12871  xaddval  12886  xmulval  12888  xrinfmss  12973  hashgval  13975  hashinf  13977  hashfxnn0  13979  pcval  16473  pc0  16483  ramcl2  16645  iccpnfhmeo  24014  taylfval  25423  xrlimcnp  26023  xrge0iifcv  31786  xrge0iifiso  31787  xrge0iifhom  31789  sge0f1o  43810  sge0sup  43819  sge0pnfmpt  43873