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