Theorem mnfnre

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

	Ref	Expression
Assertion	mnfnre	⊢ -∞ ∉ ℝ

Proof

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