Metamath Proof Explorer

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 ∘ − ↾ J × J
icccmpALT.3 ⊢ T = MetOpen ⁡ M
Assertion icccmpALT ⊢ A ∈ ℝ ∧ B ∈ ℝ → T ∈ Comp

Proof

Step Hyp Ref Expression
1 icccmpALT.1 ⊢ J = A B
2 icccmpALT.2 ⊢ M = abs ∘ − ↾ J × J
3 icccmpALT.3 ⊢ T = MetOpen ⁡ M
4 icccld ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
5 1 4 eqeltrid ⊢ A ∈ ℝ ∧ B ∈ ℝ → J ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
6 1 2 iccbnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → M ∈ Bnd ⁡ J
7 iccssre ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ⊆ ℝ
8 1 7 eqsstrid ⊢ A ∈ ℝ ∧ B ∈ ℝ → J ⊆ ℝ
9 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
10 2 3 9 reheibor ⊢ J ⊆ ℝ → T ∈ Comp ↔ J ∈ Clsd ⁡ topGen ⁡ ran ⁡ . ∧ M ∈ Bnd ⁡ J
11 8 10 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → T ∈ Comp ↔ J ∈ Clsd ⁡ topGen ⁡ ran ⁡ . ∧ M ∈ Bnd ⁡ J
12 5 6 11 mpbir2and ⊢ A ∈ ℝ ∧ B ∈ ℝ → T ∈ Comp