Metamath Proof Explorer

Theorem hlimcaui

Description: If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. (Contributed by NM, 17-Aug-1999) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlimcaui 
|- ( F ~~>v A -> F e. Cauchy )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
2 eqid 
 |-  ( IndMet ` <. <. +h , .h >. , normh >. ) = ( IndMet ` <. <. +h , .h >. , normh >. )
3 eqid 
 |-  ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) = ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) )
4 1 2 3 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) )
5 resss 
 |-  ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) ) C_ ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) )
6 4 5 eqsstri 
 |-  ~~>v C_ ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) )
7 dmss 
 |-  ( ~~>v C_ ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) -> dom ~~>v C_ dom ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) )
8 6 7 ax-mp 
 |-  dom ~~>v C_ dom ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) )
9 1 2 hhxmet 
 |-  ( IndMet ` <. <. +h , .h >. , normh >. ) e. ( *Met ` ~H )
10 3 lmcau 
 |-  ( ( IndMet ` <. <. +h , .h >. , normh >. ) e. ( *Met ` ~H ) -> dom ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) C_ ( Cau ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) )
11 9 10 ax-mp 
 |-  dom ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) C_ ( Cau ` ( IndMet ` <. <. +h , .h >. , normh >. ) )
12 8 11 sstri 
 |-  dom ~~>v C_ ( Cau ` ( IndMet ` <. <. +h , .h >. , normh >. ) )
13 4 dmeqi 
 |-  dom ~~>v = dom ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) )
14 dmres 
 |-  dom ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) ) = ( ( ~H ^m NN ) i^i dom ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) )
15 13 14 eqtri 
 |-  dom ~~>v = ( ( ~H ^m NN ) i^i dom ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) )
16 inss1 
 |-  ( ( ~H ^m NN ) i^i dom ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) ) C_ ( ~H ^m NN )
17 15 16 eqsstri 
 |-  dom ~~>v C_ ( ~H ^m NN )
18 12 17 ssini 
 |-  dom ~~>v C_ ( ( Cau ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) i^i ( ~H ^m NN ) )
19 1 2 hhcau 
 |-  Cauchy = ( ( Cau ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) i^i ( ~H ^m NN ) )
20 18 19 sseqtrri 
 |-  dom ~~>v C_ Cauchy
21 relres 
 |-  Rel ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) )
22 4 releqi 
 |-  ( Rel ~~>v <-> Rel ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) ) )
23 21 22 mpbir 
 |-  Rel ~~>v
24 23 releldmi 
 |-  ( F ~~>v A -> F e. dom ~~>v )
25 20 24 sselid 
 |-  ( F ~~>v A -> F e. Cauchy )