Theorem pnfex 11237

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 11220	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11156	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7726	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5339	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2860	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2144  Vcvv 3456  𝒫 cpw 4557  ∪ cuni 4867  ℂcc 11073  +∞cpnf 11215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pow 5324  ax-un 7720  ax-cnex 11131

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-pw 4559  df-uni 4868  df-pnf 11220

This theorem is referenced by:  pnfxr  11238  mnfxr  11241  elxnn0  12558  elxr  13120  xnegex  13213  xaddval  13228  xmulval  13230  xrinfmss  13315  hashgval  14348  hashinf  14350  hashfxnn0  14352  pcval  16882  pc0  16892  ramcl2  17054  iccpnfhmeo  25009  taylfval  26424  xrlimcnp  27035  xrge0iifcv  34233  xrge0iifiso  34234  xrge0iifhom  34236  sge0f1o  46961  sge0sup  46970  sge0pnfmpt  47024