Theorem pnfex

Description: Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018) (Revised by Steven Nguyen, 7-Dec-2022)

	Ref	Expression
Assertion	pnfex	$$⊢\mathrm{+\infty }\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-pnf	$$⊢\mathrm{+\infty }=𝒫\bigcup ℂ$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3	2	uniex	$$⊢\bigcup ℂ\in \mathrm{V}$$
4	3	pwex	$$⊢𝒫\bigcup ℂ\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢\mathrm{+\infty }\in \mathrm{V}$$