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 +∞ −∞ =

Proof

Step Hyp Ref Expression
1 disj +∞ −∞ = x ¬ x +∞ −∞
2 renepnf x x +∞
3 renemnf x x −∞
4 2 3 nelprd x ¬ x +∞ −∞
5 1 4 mprgbir +∞ −∞ =