Theorem pnfex 11343

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 11326	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11265	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7776	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5398	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2840	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488  𝒫 cpw 4622  ∪ cuni 4931  ℂcc 11182  +∞cpnf 11321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624  df-uni 4932  df-pnf 11326

This theorem is referenced by:  pnfxr  11344  mnfxr  11347  elxnn0  12627  elxr  13179  xnegex  13270  xaddval  13285  xmulval  13287  xrinfmss  13372  hashgval  14382  hashinf  14384  hashfxnn0  14386  pcval  16891  pc0  16901  ramcl2  17063  iccpnfhmeo  24995  taylfval  26418  xrlimcnp  27029  xrge0iifcv  33880  xrge0iifiso  33881  xrge0iifhom  33883  sge0f1o  46303  sge0sup  46312  sge0pnfmpt  46366