Theorem pnfex 11293

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 11276	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11215	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7740	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5355	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2831	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3464  𝒫 cpw 4580  ∪ cuni 4888  ℂcc 11132  +∞cpnf 11271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-pow 5340  ax-un 7734  ax-cnex 11190

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-pw 4582  df-uni 4889  df-pnf 11276

This theorem is referenced by:  pnfxr  11294  mnfxr  11297  elxnn0  12581  elxr  13137  xnegex  13229  xaddval  13244  xmulval  13246  xrinfmss  13331  hashgval  14356  hashinf  14358  hashfxnn0  14360  pcval  16869  pc0  16879  ramcl2  17041  iccpnfhmeo  24899  taylfval  26323  xrlimcnp  26935  xrge0iifcv  33970  xrge0iifiso  33971  xrge0iifhom  33973  sge0f1o  46378  sge0sup  46387  sge0pnfmpt  46441