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