Theorem pnfex 11028

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 11011	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 10952	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7594	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5303	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2835	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432  𝒫 cpw 4533  ∪ cuni 4839  ℂcc 10869  +∞cpnf 11006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-pow 5288  ax-un 7588  ax-cnex 10927

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535  df-uni 4840  df-pnf 11011

This theorem is referenced by:  pnfxr  11029  mnfxr  11032  elxnn0  12307  elxr  12852  xnegex  12942  xaddval  12957  xmulval  12959  xrinfmss  13044  hashgval  14047  hashinf  14049  hashfxnn0  14051  pcval  16545  pc0  16555  ramcl2  16717  iccpnfhmeo  24108  taylfval  25518  xrlimcnp  26118  xrge0iifcv  31884  xrge0iifiso  31885  xrge0iifhom  31887  sge0f1o  43920  sge0sup  43929  sge0pnfmpt  43983