Theorem pnfex 11289

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 11272	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11208	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7746	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5349	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2858	1 ⊢ +∞ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  𝒫 cpw 4560  ∪ cuni 4870  ℂcc 11125  +∞cpnf 11267

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-un 7739  ax-cnex 11183

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-pw 4562  df-uni 4871  df-pnf 11272

This theorem is used by:  pnfxr  11290  mnfxr  11293  elxnn0  12606  elxr  13169  xnegex  13262  xaddval  13277  xmulval  13279  xrinfmss  13364  hashgval  14399  hashinf  14401  hashfxnn0  14403  pcval  16940  pc0  16950  ramcl2  17112  iccpnfhmeo  25174  taylfval  26592  xrlimcnp  27203  xrge0iifcv  34431  xrge0iifiso  34432  xrge0iifhom  34434  sge0f1o  47197  sge0sup  47206  sge0pnfmpt  47260