Theorem icccmpALT

Description: A closed interval in RR is compact. Alternate proof of icccmp using the Heine-Borel theorem heibor . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Aug-2014) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	icccmpALT.1	|- J = ( A [,] B )
	icccmpALT.2	|- M = ( ( abs o. - ) |` ( J X. J ) )
	icccmpALT.3	|- T = ( MetOpen ` M )
Assertion	icccmpALT	|- ( ( A e. RR /\ B e. RR ) -> T e. Comp )

Proof

Step	Hyp	Ref	Expression
1		icccmpALT.1	|- J = ( A [,] B )
2		icccmpALT.2	|- M = ( ( abs o. - ) |` ( J X. J ) )
3		icccmpALT.3	|- T = ( MetOpen ` M )
4		icccld	|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
5	1 4	eqeltrid	|- ( ( A e. RR /\ B e. RR ) -> J e. ( Clsd ` ( topGen ` ran (,) ) ) )
6	1 2	iccbnd	|- ( ( A e. RR /\ B e. RR ) -> M e. ( Bnd ` J ) )
7		iccssre	|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
8	1 7	eqsstrid	|- ( ( A e. RR /\ B e. RR ) -> J C_ RR )
9		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
10	2 3 9	reheibor	|- ( J C_ RR -> ( T e. Comp <-> ( J e. ( Clsd ` ( topGen ` ran (,) ) ) /\ M e. ( Bnd ` J ) ) ) )
11	8 10	syl	|- ( ( A e. RR /\ B e. RR ) -> ( T e. Comp <-> ( J e. ( Clsd ` ( topGen ` ran (,) ) ) /\ M e. ( Bnd ` J ) ) ) )
12	5 6 11	mpbir2and	|- ( ( A e. RR /\ B e. RR ) -> T e. Comp )