Theorem pnfex 11203

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 11186	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11125	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7697	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5330	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2824	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444  𝒫 cpw 4559  ∪ cuni 4867  ℂcc 11042  +∞cpnf 11181

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-pow 5315  ax-un 7691  ax-cnex 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-pw 4561  df-uni 4868  df-pnf 11186

This theorem is referenced by:  pnfxr  11204  mnfxr  11207  elxnn0  12493  elxr  13052  xnegex  13144  xaddval  13159  xmulval  13161  xrinfmss  13246  hashgval  14274  hashinf  14276  hashfxnn0  14278  pcval  16791  pc0  16801  ramcl2  16963  iccpnfhmeo  24819  taylfval  26242  xrlimcnp  26854  xrge0iifcv  33897  xrge0iifiso  33898  xrge0iifhom  33900  sge0f1o  46353  sge0sup  46362  sge0pnfmpt  46416