Theorem pnfex 11262

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 11245	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11181	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7740	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5352	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2865	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3461  𝒫 cpw 4565  ∪ cuni 4874  ℂcc 11098  +∞cpnf 11240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pow 5337  ax-un 7733  ax-cnex 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-pw 4567  df-uni 4875  df-pnf 11245

This theorem is referenced by:  pnfxr  11263  mnfxr  11266  elxnn0  12579  elxr  13141  xnegex  13234  xaddval  13249  xmulval  13251  xrinfmss  13336  hashgval  14369  hashinf  14371  hashfxnn0  14373  pcval  16904  pc0  16914  ramcl2  17076  iccpnfhmeo  25073  taylfval  26488  xrlimcnp  27099  xrge0iifcv  34269  xrge0iifiso  34270  xrge0iifhom  34272  sge0f1o  47023  sge0sup  47032  sge0pnfmpt  47086