Theorem pnfex 10851

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 10834	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 10775	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7507	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5258	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2827	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2112  Vcvv 3398  𝒫 cpw 4499  ∪ cuni 4805  ℂcc 10692  +∞cpnf 10829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-pow 5243  ax-un 7501  ax-cnex 10750

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-pw 4501  df-uni 4806  df-pnf 10834

This theorem is referenced by:  pnfxr  10852  mnfxr  10855  elxnn0  12129  elxr  12673  xnegex  12763  xaddval  12778  xmulval  12780  xrinfmss  12865  hashgval  13864  hashinf  13866  hashfxnn0  13868  pcval  16360  pc0  16370  ramcl2  16532  iccpnfhmeo  23796  taylfval  25205  xrlimcnp  25805  xrge0iifcv  31552  xrge0iifiso  31553  xrge0iifhom  31555  sge0f1o  43538  sge0sup  43547  sge0pnfmpt  43601