Theorem pnfex 10694

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 10677	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 10618	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7467	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5281	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2909	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494  𝒫 cpw 4539  ∪ cuni 4838  ℂcc 10535  +∞cpnf 10672

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-pow 5266  ax-un 7461  ax-cnex 10593

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541  df-uni 4839  df-pnf 10677

This theorem is referenced by:  pnfxr  10695  mnfxr  10698  elxnn0  11970  elxr  12512  xnegex  12602  xaddval  12617  xmulval  12619  xrinfmss  12704  hashgval  13694  hashinf  13696  hashfxnn0  13698  pcval  16181  pc0  16191  ramcl2  16352  iccpnfhmeo  23549  taylfval  24947  xrlimcnp  25546  xrge0iifcv  31177  xrge0iifiso  31178  xrge0iifhom  31180  sge0f1o  42684  sge0sup  42693  sge0pnfmpt  42747