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