Theorem pnfex 11227

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 11210	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11149	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7717	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5335	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2824	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447  𝒫 cpw 4563  ∪ cuni 4871  ℂcc 11066  +∞cpnf 11205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-pow 5320  ax-un 7711  ax-cnex 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565  df-uni 4872  df-pnf 11210

This theorem is referenced by:  pnfxr  11228  mnfxr  11231  elxnn0  12517  elxr  13076  xnegex  13168  xaddval  13183  xmulval  13185  xrinfmss  13270  hashgval  14298  hashinf  14300  hashfxnn0  14302  pcval  16815  pc0  16825  ramcl2  16987  iccpnfhmeo  24843  taylfval  26266  xrlimcnp  26878  xrge0iifcv  33924  xrge0iifiso  33925  xrge0iifhom  33927  sge0f1o  46380  sge0sup  46389  sge0pnfmpt  46443