Theorem pnfex 11157

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 11140	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11079	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7669	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5316	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2825	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2110  Vcvv 3434  𝒫 cpw 4548  ∪ cuni 4857  ℂcc 10996  +∞cpnf 11135

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 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-pow 5301  ax-un 7663  ax-cnex 11054

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-ss 3917  df-pw 4550  df-uni 4858  df-pnf 11140

This theorem is referenced by:  pnfxr  11158  mnfxr  11161  elxnn0  12448  elxr  13007  xnegex  13099  xaddval  13114  xmulval  13116  xrinfmss  13201  hashgval  14232  hashinf  14234  hashfxnn0  14236  pcval  16748  pc0  16758  ramcl2  16920  iccpnfhmeo  24863  taylfval  26286  xrlimcnp  26898  xrge0iifcv  33937  xrge0iifiso  33938  xrge0iifhom  33940  sge0f1o  46399  sge0sup  46408  sge0pnfmpt  46462