Metamath Proof Explorer

Theorem rrnheibor

Description: Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses rrnheibor.1 ⊢ X = ℝ I
rrnheibor.2 ⊢ M = ℝ n ⁡ I ↾ Y × Y
rrnheibor.3 ⊢ T = MetOpen ⁡ M
rrnheibor.4 ⊢ U = MetOpen ⁡ ℝ n ⁡ I
Assertion rrnheibor ⊢ I ∈ Fin ∧ Y ⊆ X → T ∈ Comp ↔ Y ∈ Clsd ⁡ U ∧ M ∈ Bnd ⁡ Y

Proof

Step Hyp Ref Expression
1 rrnheibor.1 ⊢ X = ℝ I
2 rrnheibor.2 ⊢ M = ℝ n ⁡ I ↾ Y × Y
3 rrnheibor.3 ⊢ T = MetOpen ⁡ M
4 rrnheibor.4 ⊢ U = MetOpen ⁡ ℝ n ⁡ I
5 1 rrnmet ⊢ I ∈ Fin → ℝ n ⁡ I ∈ Met ⁡ X
6 metres2 ⊢ ℝ n ⁡ I ∈ Met ⁡ X ∧ Y ⊆ X → ℝ n ⁡ I ↾ Y × Y ∈ Met ⁡ Y
7 2 6 eqeltrid ⊢ ℝ n ⁡ I ∈ Met ⁡ X ∧ Y ⊆ X → M ∈ Met ⁡ Y
8 5 7 sylan ⊢ I ∈ Fin ∧ Y ⊆ X → M ∈ Met ⁡ Y
9 8 biantrurd ⊢ I ∈ Fin ∧ Y ⊆ X → T ∈ Comp ↔ M ∈ Met ⁡ Y ∧ T ∈ Comp
10 3 heibor ⊢ M ∈ Met ⁡ Y ∧ T ∈ Comp ↔ M ∈ CMet ⁡ Y ∧ M ∈ TotBnd ⁡ Y
11 9 10 bitrdi ⊢ I ∈ Fin ∧ Y ⊆ X → T ∈ Comp ↔ M ∈ CMet ⁡ Y ∧ M ∈ TotBnd ⁡ Y
12 2 eleq1i ⊢ M ∈ CMet ⁡ Y ↔ ℝ n ⁡ I ↾ Y × Y ∈ CMet ⁡ Y
13 1 rrncms ⊢ I ∈ Fin → ℝ n ⁡ I ∈ CMet ⁡ X
14 13 adantr ⊢ I ∈ Fin ∧ Y ⊆ X → ℝ n ⁡ I ∈ CMet ⁡ X
15 4 cmetss ⊢ ℝ n ⁡ I ∈ CMet ⁡ X → ℝ n ⁡ I ↾ Y × Y ∈ CMet ⁡ Y ↔ Y ∈ Clsd ⁡ U
16 14 15 syl ⊢ I ∈ Fin ∧ Y ⊆ X → ℝ n ⁡ I ↾ Y × Y ∈ CMet ⁡ Y ↔ Y ∈ Clsd ⁡ U
17 12 16 syl5bb ⊢ I ∈ Fin ∧ Y ⊆ X → M ∈ CMet ⁡ Y ↔ Y ∈ Clsd ⁡ U
18 1 2 rrntotbnd ⊢ I ∈ Fin → M ∈ TotBnd ⁡ Y ↔ M ∈ Bnd ⁡ Y
19 18 adantr ⊢ I ∈ Fin ∧ Y ⊆ X → M ∈ TotBnd ⁡ Y ↔ M ∈ Bnd ⁡ Y
20 17 19 anbi12d ⊢ I ∈ Fin ∧ Y ⊆ X → M ∈ CMet ⁡ Y ∧ M ∈ TotBnd ⁡ Y ↔ Y ∈ Clsd ⁡ U ∧ M ∈ Bnd ⁡ Y
21 11 20 bitrd ⊢ I ∈ Fin ∧ Y ⊆ X → T ∈ Comp ↔ Y ∈ Clsd ⁡ U ∧ M ∈ Bnd ⁡ Y