Theorem pnfex 11165

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 11148	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11087	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7674	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5316	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2827	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  𝒫 cpw 4547  ∪ cuni 4856  ℂcc 11004  +∞cpnf 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-pow 5301  ax-un 7668  ax-cnex 11062

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-pw 4549  df-uni 4857  df-pnf 11148

This theorem is referenced by:  pnfxr  11166  mnfxr  11169  elxnn0  12456  elxr  13015  xnegex  13107  xaddval  13122  xmulval  13124  xrinfmss  13209  hashgval  14240  hashinf  14242  hashfxnn0  14244  pcval  16756  pc0  16766  ramcl2  16928  iccpnfhmeo  24870  taylfval  26293  xrlimcnp  26905  xrge0iifcv  33947  xrge0iifiso  33948  xrge0iifhom  33950  sge0f1o  46490  sge0sup  46499  sge0pnfmpt  46553