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 = ( RR ^m I )
rrnheibor.2
|- M = ( ( Rn ` I ) |` ( Y X. Y ) )
rrnheibor.3
|- T = ( MetOpen ` M )
rrnheibor.4
|- U = ( MetOpen ` ( Rn ` I ) )
Assertion rrnheibor
|- ( ( I e. Fin /\ Y C_ X ) -> ( T e. Comp <-> ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 rrnheibor.1
 |-  X = ( RR ^m I )
2 rrnheibor.2
 |-  M = ( ( Rn ` I ) |` ( Y X. Y ) )
3 rrnheibor.3
 |-  T = ( MetOpen ` M )
4 rrnheibor.4
 |-  U = ( MetOpen ` ( Rn ` I ) )
5 1 rrnmet
 |-  ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
6 metres2
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ Y C_ X ) -> ( ( Rn ` I ) |` ( Y X. Y ) ) e. ( Met ` Y ) )
7 2 6 eqeltrid
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ Y C_ X ) -> M e. ( Met ` Y ) )
8 5 7 sylan
 |-  ( ( I e. Fin /\ Y C_ X ) -> M e. ( Met ` Y ) )
9 8 biantrurd
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( T e. Comp <-> ( M e. ( Met ` Y ) /\ T e. Comp ) ) )
10 3 heibor
 |-  ( ( M e. ( Met ` Y ) /\ T e. Comp ) <-> ( M e. ( CMet ` Y ) /\ M e. ( TotBnd ` Y ) ) )
11 9 10 bitrdi
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( T e. Comp <-> ( M e. ( CMet ` Y ) /\ M e. ( TotBnd ` Y ) ) ) )
12 2 eleq1i
 |-  ( M e. ( CMet ` Y ) <-> ( ( Rn ` I ) |` ( Y X. Y ) ) e. ( CMet ` Y ) )
13 1 rrncms
 |-  ( I e. Fin -> ( Rn ` I ) e. ( CMet ` X ) )
14 13 adantr
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( Rn ` I ) e. ( CMet ` X ) )
15 4 cmetss
 |-  ( ( Rn ` I ) e. ( CMet ` X ) -> ( ( ( Rn ` I ) |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` U ) ) )
16 14 15 syl
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( ( ( Rn ` I ) |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` U ) ) )
17 12 16 syl5bb
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( M e. ( CMet ` Y ) <-> Y e. ( Clsd ` U ) ) )
18 1 2 rrntotbnd
 |-  ( I e. Fin -> ( M e. ( TotBnd ` Y ) <-> M e. ( Bnd ` Y ) ) )
19 18 adantr
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( M e. ( TotBnd ` Y ) <-> M e. ( Bnd ` Y ) ) )
20 17 19 anbi12d
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( ( M e. ( CMet ` Y ) /\ M e. ( TotBnd ` Y ) ) <-> ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) ) )
21 11 20 bitrd
 |-  ( ( I e. Fin /\ Y C_ X ) -> ( T e. Comp <-> ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) ) )