Theorem pnfex 11333

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 11316	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11252	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7741	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5341	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2856	1 ⊢ +∞ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  𝒫 cpw 4556  ∪ cuni 4866  ℂcc 11169  +∞cpnf 11311

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 2732  ax-sep 5248  ax-pow 5326  ax-un 7734  ax-cnex 11227

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-pw 4558  df-uni 4867  df-pnf 11316

This theorem is used by:  pnfxr  11334  mnfxr  11337  elxnn0  12650  elxr  13214  xnegex  13307  xaddval  13322  xmulval  13324  xrinfmss  13409  hashgval  14444  hashinf  14446  hashfxnn0  14448  pcval  16983  pc0  16993  ramcl2  17155  iccpnfhmeo  25227  taylfval  26649  xrlimcnp  27259  xrge0iifcv  34499  xrge0iifiso  34500  xrge0iifhom  34502  sge0f1o  47314  sge0sup  47323  sge0pnfmpt  47377