This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ +∞ ∈ V

Step	Hyp	Ref	Expression
1		df-pnf	⊢ +∞ = 𝒫 ∪ ℂ
2		cnex	⊢ ℂ ∈ V
3	2	uniex	⊢ ∪ ℂ ∈ V
4	3	pwex	⊢ 𝒫 ∪ ℂ ∈ V
5	1 4	eqeltri	⊢ +∞ ∈ V