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 
|- +oo e. RR*

Proof

Step Hyp Ref Expression
1 ssun2 
 |-  { +oo , -oo } C_ ( RR u. { +oo , -oo } )
2 pnfex 
 |-  +oo e. _V
3 2 prid1 
 |-  +oo e. { +oo , -oo }
4 1 3 sselii 
 |-  +oo e. ( RR u. { +oo , -oo } )
5 df-xr 
 |-  RR* = ( RR u. { +oo , -oo } )
6 4 5 eleqtrri 
 |-  +oo e. RR*