Theorem pnfex 11192

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 11175	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11113	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7689	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5318	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2833	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430  𝒫 cpw 4542  ∪ cuni 4851  ℂcc 11030  +∞cpnf 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pow 5303  ax-un 7683  ax-cnex 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544  df-uni 4852  df-pnf 11175

This theorem is referenced by:  pnfxr  11193  mnfxr  11196  elxnn0  12506  elxr  13061  xnegex  13154  xaddval  13169  xmulval  13171  xrinfmss  13256  hashgval  14289  hashinf  14291  hashfxnn0  14293  pcval  16809  pc0  16819  ramcl2  16981  iccpnfhmeo  24925  taylfval  26338  xrlimcnp  26948  xrge0iifcv  34097  xrge0iifiso  34098  xrge0iifhom  34100  sge0f1o  46831  sge0sup  46840  sge0pnfmpt  46894