Theorem pnfex 11386

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 11369	. 2 ⊢ +∞ = 𝒫 ∪ ℂ
2		cnex 11305	. . . 4 ⊢ ℂ ∈ V
3	2	uniex 7779	. . 3 ⊢ ∪ ℂ ∈ V
4	3	pwex 5346	. 2 ⊢ 𝒫 ∪ ℂ ∈ V
5	1, 4	eqeltri 2860	1 ⊢ +∞ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  𝒫 cpw 4560  ∪ cuni 4870  ℂcc 11222  +∞cpnf 11364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-un 7772  ax-cnex 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562  df-uni 4871  df-pnf 11369

This theorem is used by:  pnfxr  11387  mnfxr  11390  elxnn0  12705  elxr  13269  xnegex  13362  xaddval  13377  xmulval  13379  xrinfmss  13464  hashgval  14501  hashinf  14503  hashfxnn0  14505  pcval  17048  pc0  17058  ramcl2  17220  iccpnfhmeo  25293  taylfval  26713  xrlimcnp  27323  xrge0iifcv  34633  xrge0iifiso  34634  xrge0iifhom  34636  sge0f1o  47595  sge0sup  47604  sge0pnfmpt  47658