Theorem pnfnre

Description: Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005)

	Ref	Expression
Assertion	pnfnre	⊢ +∞ ∉ ℝ

Proof

Step	Hyp	Ref	Expression
1		df-pnf	⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel	⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1 2	eqneltri	⊢ ¬ +∞ ∈ ℂ
4		recn	⊢ ( +∞ ∈ ℝ → +∞ ∈ ℂ )
5	3 4	mto	⊢ ¬ +∞ ∈ ℝ
6	5	nelir	⊢ +∞ ∉ ℝ