Theorem pnfex 11193

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 11176	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11114	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7688	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5312	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2837	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2121  Vcvv 3433  𝒫 cpw 4532  ∪ cuni 4841  ℂcc 11031  +∞cpnf 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pow 5297  ax-un 7682  ax-cnex 11089

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-pw 4534  df-uni 4842  df-pnf 11176

This theorem is referenced by:  pnfxr  11194  mnfxr  11197  elxnn0  12507  elxr  13062  xnegex  13155  xaddval  13170  xmulval  13172  xrinfmss  13257  hashgval  14290  hashinf  14292  hashfxnn0  14294  pcval  16810  pc0  16820  ramcl2  16982  iccpnfhmeo  24934  taylfval  26346  xrlimcnp  26954  xrge0iifcv  34130  xrge0iifiso  34131  xrge0iifhom  34133  sge0f1o  46839  sge0sup  46848  sge0pnfmpt  46902