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 ‘ 𝑌 ) ) ) )