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 +∞ *

Proof

Step Hyp Ref Expression
1 ssun2 +∞ −∞ +∞ −∞
2 pnfex +∞ V
3 2 prid1 +∞ +∞ −∞
4 1 3 sselii +∞ +∞ −∞
5 df-xr * = +∞ −∞
6 4 5 eleqtrri +∞ *