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