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

Metamath Proof Explorer

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 \{+∞, −∞\} = \emptyset$

Step	Hyp	Ref	Expression
1		disj	$⊢ ℝ \cap \{+∞, −∞\} = \emptyset \leftrightarrow \forall x \in ℝ \neg x \in \{+∞, −∞\}$
2		renepnf	$⊢ x \in ℝ \to x \neq +∞$
3		renemnf	$⊢ x \in ℝ \to x \neq −∞$
4	2 3	nelprd	$⊢ x \in ℝ \to \neg x \in \{+∞, −∞\}$
5	1 4	mprgbir	$⊢ ℝ \cap \{+∞, −∞\} = \emptyset$