Theorem pnfex 11290

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 11273	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11209	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7747	. . 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 11126  +∞cpnf 11268

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 7740  ax-cnex 11184

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 11273

This theorem is used by:  pnfxr  11291  mnfxr  11294  elxnn0  12607  elxr  13171  xnegex  13264  xaddval  13279  xmulval  13281  xrinfmss  13366  hashgval  14401  hashinf  14403  hashfxnn0  14405  pcval  16942  pc0  16952  ramcl2  17114  iccpnfhmeo  25179  taylfval  26602  xrlimcnp  27213  xrge0iifcv  34452  xrge0iifiso  34453  xrge0iifhom  34455  sge0f1o  47218  sge0sup  47227  sge0pnfmpt  47281