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	⊢ +∞ ∈ ℝ*

Proof

Step	Hyp	Ref	Expression
1		ssun2	⊢ { +∞ , -∞ } ⊆ ( ℝ ∪ { +∞ , -∞ } )
2		pnfex	⊢ +∞ ∈ V
3	2	prid1	⊢ +∞ ∈ { +∞ , -∞ }
4	1 3	sselii	⊢ +∞ ∈ ( ℝ ∪ { +∞ , -∞ } )
5		df-xr	⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )
6	4 5	eleqtrri	⊢ +∞ ∈ ℝ*