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 ` <_ ) e. Comp

Proof

Step	Hyp	Ref	Expression
1		xrhmph	|- II ~= ( ordTop ` <_ )
2		iicmp	|- II e. Comp
3		cmphmph	|- ( II ~= ( ordTop ` <_ ) -> ( II e. Comp -> ( ordTop ` <_ ) e. Comp ) )
4	1 2 3	mp2	|- ( ordTop ` <_ ) e. Comp