Metamath Proof Explorer


Theorem hlimuni

Description: A Hilbert space sequence converges to at most one limit. (Contributed by NM, 19-Aug-1999) (Revised by Mario Carneiro, 2-May-2015) (New usage is discouraged.)

Ref Expression
Assertion hlimuni
|- ( ( F ~~>v A /\ F ~~>v B ) -> A = B )

Proof

Step Hyp Ref Expression
1 hlimf
 |-  ~~>v : dom ~~>v --> ~H
2 ffun
 |-  ( ~~>v : dom ~~>v --> ~H -> Fun ~~>v )
3 funbrfv
 |-  ( Fun ~~>v -> ( F ~~>v A -> ( ~~>v ` F ) = A ) )
4 1 2 3 mp2b
 |-  ( F ~~>v A -> ( ~~>v ` F ) = A )
5 funbrfv
 |-  ( Fun ~~>v -> ( F ~~>v B -> ( ~~>v ` F ) = B ) )
6 1 2 5 mp2b
 |-  ( F ~~>v B -> ( ~~>v ` F ) = B )
7 4 6 sylan9req
 |-  ( ( F ~~>v A /\ F ~~>v B ) -> A = B )