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	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$

Proof

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