Theorem pnfex 11314

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 11297	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11236	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7761	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5380	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2837	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480  𝒫 cpw 4600  ∪ cuni 4907  ℂcc 11153  +∞cpnf 11292

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pow 5365  ax-un 7755  ax-cnex 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602  df-uni 4908  df-pnf 11297

This theorem is referenced by:  pnfxr  11315  mnfxr  11318  elxnn0  12601  elxr  13158  xnegex  13250  xaddval  13265  xmulval  13267  xrinfmss  13352  hashgval  14372  hashinf  14374  hashfxnn0  14376  pcval  16882  pc0  16892  ramcl2  17054  iccpnfhmeo  24976  taylfval  26400  xrlimcnp  27011  xrge0iifcv  33933  xrge0iifiso  33934  xrge0iifhom  33936  sge0f1o  46397  sge0sup  46406  sge0pnfmpt  46460