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	⊢ 𝐽 = ( 𝐴 [,] 𝐵 )
	icccmpALT.2	⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) )
	icccmpALT.3	⊢ 𝑇 = ( MetOpen ‘ 𝑀 )
Assertion	icccmpALT	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑇 ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		icccmpALT.1	⊢ 𝐽 = ( 𝐴 [,] 𝐵 )
2		icccmpALT.2	⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) )
3		icccmpALT.3	⊢ 𝑇 = ( MetOpen ‘ 𝑀 )
4		icccld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
5	1 4	eqeltrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐽 ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
6	1 2	iccbnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑀 ∈ ( Bnd ‘ 𝐽 ) )
7		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
8	1 7	eqsstrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐽 ⊆ ℝ )
9		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
10	2 3 9	reheibor	⊢ ( 𝐽 ⊆ ℝ → ( 𝑇 ∈ Comp ↔ ( 𝐽 ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ∧ 𝑀 ∈ ( Bnd ‘ 𝐽 ) ) ) )
11	8 10	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑇 ∈ Comp ↔ ( 𝐽 ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ∧ 𝑀 ∈ ( Bnd ‘ 𝐽 ) ) ) )
12	5 6 11	mpbir2and	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑇 ∈ Comp )