Theorem pnfex 11362

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  𝒫 cpw 4556  ∪ cuni 4866  ℂcc 11198  +∞cpnf 11340

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-un 7751  ax-cnex 11256

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558  df-uni 4867  df-pnf 11345

This theorem is used by:  pnfxr  11363  mnfxr  11366  elxnn0  12681  elxr  13245  xnegex  13338  xaddval  13353  xmulval  13355  xrinfmss  13440  hashgval  14477  hashinf  14479  hashfxnn0  14481  pcval  17022  pc0  17032  ramcl2  17194  iccpnfhmeo  25266  taylfval  26686  xrlimcnp  27296  xrge0iifcv  34566  xrge0iifiso  34567  xrge0iifhom  34569  sge0f1o  47392  sge0sup  47401  sge0pnfmpt  47455