Theorem pnfex 11185

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 11168	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11107	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7686	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5325	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2832	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440  𝒫 cpw 4554  ∪ cuni 4863  ℂcc 11024  +∞cpnf 11163

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pow 5310  ax-un 7680  ax-cnex 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556  df-uni 4864  df-pnf 11168

This theorem is referenced by:  pnfxr  11186  mnfxr  11189  elxnn0  12476  elxr  13030  xnegex  13123  xaddval  13138  xmulval  13140  xrinfmss  13225  hashgval  14256  hashinf  14258  hashfxnn0  14260  pcval  16772  pc0  16782  ramcl2  16944  iccpnfhmeo  24899  taylfval  26322  xrlimcnp  26934  xrge0iifcv  34091  xrge0iifiso  34092  xrge0iifhom  34094  sge0f1o  46636  sge0sup  46645  sge0pnfmpt  46699