Theorem pnfex 11183

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 11166	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11105	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7684	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5323	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2830	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3438  𝒫 cpw 4552  ∪ cuni 4861  ℂcc 11022  +∞cpnf 11161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pow 5308  ax-un 7678  ax-cnex 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-pw 4554  df-uni 4862  df-pnf 11166

This theorem is referenced by:  pnfxr  11184  mnfxr  11187  elxnn0  12474  elxr  13028  xnegex  13121  xaddval  13136  xmulval  13138  xrinfmss  13223  hashgval  14254  hashinf  14256  hashfxnn0  14258  pcval  16770  pc0  16780  ramcl2  16942  iccpnfhmeo  24897  taylfval  26320  xrlimcnp  26932  xrge0iifcv  34040  xrge0iifiso  34041  xrge0iifhom  34043  sge0f1o  46568  sge0sup  46577  sge0pnfmpt  46631