Theorem renfdisj

Description: The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

	Ref	Expression
Assertion	renfdisj	⊢ ( ℝ ∩ { +∞ , -∞ } ) = ∅

Proof

Step	Hyp	Ref	Expression
1		disj	⊢ ( ( ℝ ∩ { +∞ , -∞ } ) = ∅ ↔ ∀ 𝑥 ∈ ℝ ¬ 𝑥 ∈ { +∞ , -∞ } )
2		renepnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 ≠ +∞ )
3		renemnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 ≠ -∞ )
4	2 3	nelprd	⊢ ( 𝑥 ∈ ℝ → ¬ 𝑥 ∈ { +∞ , -∞ } )
5	1 4	mprgbir	⊢ ( ℝ ∩ { +∞ , -∞ } ) = ∅