Theorem pnfex 10696

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 10679	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 10620	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7469	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5283	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2911	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3496  𝒫 cpw 4541  ∪ cuni 4840  ℂcc 10537  +∞cpnf 10674

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 2795  ax-sep 5205  ax-pow 5268  ax-un 7463  ax-cnex 10595

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543  df-uni 4841  df-pnf 10679

This theorem is referenced by:  pnfxr  10697  mnfxr  10700  elxnn0  11972  elxr  12514  xnegex  12604  xaddval  12619  xmulval  12621  xrinfmss  12706  hashgval  13696  hashinf  13698  hashfxnn0  13700  pcval  16183  pc0  16193  ramcl2  16354  iccpnfhmeo  23551  taylfval  24949  xrlimcnp  25548  xrge0iifcv  31179  xrge0iifiso  31180  xrge0iifhom  31182  sge0f1o  42671  sge0sup  42680  sge0pnfmpt  42734