Theorem pnfex 10499

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 10482	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 10422	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7289	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5138	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2864	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2051  Vcvv 3417  𝒫 cpw 4425  ∪ cuni 4717  ℂcc 10339  +∞cpnf 10477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752  ax-sep 5064  ax-pow 5123  ax-un 7285  ax-cnex 10397

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-rex 3096  df-v 3419  df-in 3838  df-ss 3845  df-pw 4427  df-uni 4718  df-pnf 10482

This theorem is referenced by:  pnfxr  10500  mnfxr  10504  elxnn0  11787  elxr  12334  xnegex  12424  xaddval  12439  xmulval  12441  xrinfmss  12525  hashgval  13514  hashinf  13516  hashfxnn0  13518  pcval  16043  pc0  16053  ramcl2  16214  iccpnfhmeo  23267  taylfval  24665  xrlimcnp  25263  xrge0iifcv  30853  xrge0iifiso  30854  xrge0iifhom  30856  sge0f1o  42130  sge0sup  42139  sge0pnfmpt  42193