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

Metamath Proof Explorer

Theorem pnfxr

Description: Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005) (Proof shortened by Anthony Hart, 29-Aug-2011)

		Ref	Expression
	Assertion	pnfxr	$⊢ +∞ \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		ssun2	$⊢ \{+∞, −∞\} \subseteq ℝ \cup \{+∞, −∞\}$
2		pnfex	$⊢ +∞ \in V$
3	2	prid1	$⊢ +∞ \in \{+∞, −∞\}$
4	1 3	sselii	$⊢ +∞ \in (ℝ \cup \{+∞, −∞\})$
5		df-xr	$⊢ ℝ^{*} = ℝ \cup \{+∞, −∞\}$
6	4 5	eleqtrri	$⊢ +∞ \in ℝ^{*}$