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 ( 𝐹 ⇝𝑣 𝐴 β†’ 𝐹 ∈ Cauchy )

Proof

Step Hyp Ref Expression
1 eqid ⊒ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ = ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩
2 eqid ⊒ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) = ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ )
3 eqid ⊒ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) = ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) )
4 1 2 3 hhlm ⊒ ⇝𝑣 = ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) β†Ύ ( β„‹ ↑m β„• ) )
5 resss ⊒ ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) β†Ύ ( β„‹ ↑m β„• ) ) βŠ† ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) )
6 4 5 eqsstri ⊒ ⇝𝑣 βŠ† ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) )
7 dmss ⊒ ( ⇝𝑣 βŠ† ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) β†’ dom ⇝𝑣 βŠ† dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) )
8 6 7 ax-mp ⊒ dom ⇝𝑣 βŠ† dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) )
9 1 2 hhxmet ⊒ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ∈ ( ∞Met β€˜ β„‹ )
10 3 lmcau ⊒ ( ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ∈ ( ∞Met β€˜ β„‹ ) β†’ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) βŠ† ( Cau β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) )
11 9 10 ax-mp ⊒ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) βŠ† ( Cau β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) )
12 8 11 sstri ⊒ dom ⇝𝑣 βŠ† ( Cau β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) )
13 4 dmeqi ⊒ dom ⇝𝑣 = dom ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) β†Ύ ( β„‹ ↑m β„• ) )
14 dmres ⊒ dom ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) β†Ύ ( β„‹ ↑m β„• ) ) = ( ( β„‹ ↑m β„• ) ∩ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) )
15 13 14 eqtri ⊒ dom ⇝𝑣 = ( ( β„‹ ↑m β„• ) ∩ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) )
16 inss1 ⊒ ( ( β„‹ ↑m β„• ) ∩ dom ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) ) βŠ† ( β„‹ ↑m β„• )
17 15 16 eqsstri ⊒ dom ⇝𝑣 βŠ† ( β„‹ ↑m β„• )
18 12 17 ssini ⊒ dom ⇝𝑣 βŠ† ( ( Cau β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ∩ ( β„‹ ↑m β„• ) )
19 1 2 hhcau ⊒ Cauchy = ( ( Cau β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ∩ ( β„‹ ↑m β„• ) )
20 18 19 sseqtrri ⊒ dom ⇝𝑣 βŠ† Cauchy
21 relres ⊒ Rel ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) β†Ύ ( β„‹ ↑m β„• ) )
22 4 releqi ⊒ ( Rel ⇝𝑣 ↔ Rel ( ( ⇝𝑑 β€˜ ( MetOpen β€˜ ( IndMet β€˜ ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩ ) ) ) β†Ύ ( β„‹ ↑m β„• ) ) )
23 21 22 mpbir ⊒ Rel ⇝𝑣
24 23 releldmi ⊒ ( 𝐹 ⇝𝑣 𝐴 β†’ 𝐹 ∈ dom ⇝𝑣 )
25 20 24 sselid ⊒ ( 𝐹 ⇝𝑣 𝐴 β†’ 𝐹 ∈ Cauchy )