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	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Comp}$$

Proof

Step	Hyp	Ref	Expression
1		xrhmph	$$⊢\mathrm{II}\simeq \mathrm{ordTop}\left(\le \right)$$
2		iicmp	$$⊢\mathrm{II}\in \mathrm{Comp}$$
3		cmphmph	$$⊢\mathrm{II}\simeq \mathrm{ordTop}\left(\le \right)\to \left(\mathrm{II}\in \mathrm{Comp}\to \mathrm{ordTop}\left(\le \right)\in \mathrm{Comp}\right)$$
4	1 2 3	mp2	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Comp}$$