Theorem pnfex 11198

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 11181	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11119	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7695	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5322	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2832	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  𝒫 cpw 4541  ∪ cuni 4850  ℂcc 11036  +∞cpnf 11176

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 2708  ax-sep 5231  ax-pow 5307  ax-un 7689  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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543  df-uni 4851  df-pnf 11181

This theorem is referenced by:  pnfxr  11199  mnfxr  11202  elxnn0  12512  elxr  13067  xnegex  13160  xaddval  13175  xmulval  13177  xrinfmss  13262  hashgval  14295  hashinf  14297  hashfxnn0  14299  pcval  16815  pc0  16825  ramcl2  16987  iccpnfhmeo  24912  taylfval  26324  xrlimcnp  26932  xrge0iifcv  34078  xrge0iifiso  34079  xrge0iifhom  34081  sge0f1o  46810  sge0sup  46819  sge0pnfmpt  46873