Theorem pnfex 11197

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 11180	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11119	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7696	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5327	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2833	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  𝒫 cpw 4556  ∪ cuni 4865  ℂcc 11036  +∞cpnf 11175

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 5243  ax-pow 5312  ax-un 7690  ax-cnex 11094

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 3444  df-ss 3920  df-pw 4558  df-uni 4866  df-pnf 11180

This theorem is referenced by:  pnfxr  11198  mnfxr  11201  elxnn0  12488  elxr  13042  xnegex  13135  xaddval  13150  xmulval  13152  xrinfmss  13237  hashgval  14268  hashinf  14270  hashfxnn0  14272  pcval  16784  pc0  16794  ramcl2  16956  iccpnfhmeo  24911  taylfval  26334  xrlimcnp  26946  xrge0iifcv  34112  xrge0iifiso  34113  xrge0iifhom  34115  sge0f1o  46740  sge0sup  46749  sge0pnfmpt  46803