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 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
rrnheibor.2 ⊢ 𝑀 = ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) )
rrnheibor.3 ⊢ 𝑇 = ( MetOpen ‘ 𝑀 )
rrnheibor.4 ⊢ 𝑈 = ( MetOpen ‘ ( ℝn ‘ 𝐼 ) )
Assertion rrnheibor ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑇 ∈ Comp ↔ ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ∧ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 rrnheibor.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2 rrnheibor.2 ⊢ 𝑀 = ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) )
3 rrnheibor.3 ⊢ 𝑇 = ( MetOpen ‘ 𝑀 )
4 rrnheibor.4 ⊢ 𝑈 = ( MetOpen ‘ ( ℝn ‘ 𝐼 ) )
5 1 rrnmet ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) )
6 metres2 ⊢ ( ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
7 2 6 eqeltrid ⊢ ( ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑌 ) )
8 5 7 sylan ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑌 ) )
9 8 biantrurd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑇 ∈ Comp ↔ ( 𝑀 ∈ ( Met ‘ 𝑌 ) ∧ 𝑇 ∈ Comp ) ) )
10 3 heibor ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑌 ) ∧ 𝑇 ∈ Comp ) ↔ ( 𝑀 ∈ ( CMet ‘ 𝑌 ) ∧ 𝑀 ∈ ( TotBnd ‘ 𝑌 ) ) )
11 9 10 bitrdi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑇 ∈ Comp ↔ ( 𝑀 ∈ ( CMet ‘ 𝑌 ) ∧ 𝑀 ∈ ( TotBnd ‘ 𝑌 ) ) ) )
12 2 eleq1i ⊢ ( 𝑀 ∈ ( CMet ‘ 𝑌 ) ↔ ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) )
13 1 rrncms ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( CMet ‘ 𝑋 ) )
14 13 adantr ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( ℝn ‘ 𝐼 ) ∈ ( CMet ‘ 𝑋 ) )
15 4 cmetss ⊢ ( ( ℝn ‘ 𝐼 ) ∈ ( CMet ‘ 𝑋 ) → ( ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ↔ 𝑌 ∈ ( Clsd ‘ 𝑈 ) ) )
16 14 15 syl ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ↔ 𝑌 ∈ ( Clsd ‘ 𝑈 ) ) )
17 12 16 syl5bb ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑀 ∈ ( CMet ‘ 𝑌 ) ↔ 𝑌 ∈ ( Clsd ‘ 𝑈 ) ) )
18 1 2 rrntotbnd ⊢ ( 𝐼 ∈ Fin → ( 𝑀 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) )
19 18 adantr ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑀 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) )
20 17 19 anbi12d ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( ( 𝑀 ∈ ( CMet ‘ 𝑌 ) ∧ 𝑀 ∈ ( TotBnd ‘ 𝑌 ) ) ↔ ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ∧ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) ) )
21 11 20 bitrd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑇 ∈ Comp ↔ ( 𝑌 ∈ ( Clsd ‘ 𝑈 ) ∧ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) ) )