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	$$⊢ℝ\cap \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		disj	$$⊢ℝ\cap \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}=\varnothing \leftrightarrow \forall x\in ℝ\neg x\in \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$$
2		renepnf	$$⊢x\in ℝ\to x\ne \mathrm{+\infty }$$
3		renemnf	$$⊢x\in ℝ\to x\ne \mathrm{-\infty }$$
4	2 3	nelprd	$$⊢x\in ℝ\to \neg x\in \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$$
5	1 4	mprgbir	$$⊢ℝ\cap \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}=\varnothing$$