This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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