Theorem pnfex 11312

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 11295	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11234	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7760	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5386	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2835	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3478  𝒫 cpw 4605  ∪ cuni 4912  ℂcc 11151  +∞cpnf 11290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-pow 5371  ax-un 7754  ax-cnex 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-pw 4607  df-uni 4913  df-pnf 11295

This theorem is referenced by:  pnfxr  11313  mnfxr  11316  elxnn0  12599  elxr  13156  xnegex  13247  xaddval  13262  xmulval  13264  xrinfmss  13349  hashgval  14369  hashinf  14371  hashfxnn0  14373  pcval  16878  pc0  16888  ramcl2  17050  iccpnfhmeo  24990  taylfval  26415  xrlimcnp  27026  xrge0iifcv  33895  xrge0iifiso  33896  xrge0iifhom  33898  sge0f1o  46338  sge0sup  46347  sge0pnfmpt  46401