Metamath Proof Explorer

Theorem renfdisj

Description: The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion renfdisj 
|- ( RR i^i { +oo , -oo } ) = (/)

Proof

Step Hyp Ref Expression
1 disj 
 |-  ( ( RR i^i { +oo , -oo } ) = (/) <-> A. x e. RR -. x e. { +oo , -oo } )
2 renepnf 
 |-  ( x e. RR -> x =/= +oo )
3 renemnf 
 |-  ( x e. RR -> x =/= -oo )
4 2 3 nelprd 
 |-  ( x e. RR -> -. x e. { +oo , -oo } )
5 1 4 mprgbir 
 |-  ( RR i^i { +oo , -oo } ) = (/)