Metamath Proof Explorer

Theorem xrcmp

Description: The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo ), this means that RR* is a compactification of RR . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion xrcmp ordTop Comp


Step Hyp Ref Expression
1 xrhmph II ordTop
2 iicmp II Comp
3 cmphmph II ordTop II Comp ordTop Comp
4 1 2 3 mp2 ordTop Comp