Metamath Proof Explorer

Theorem climeu

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005)

Ref Expression
Assertion climeu 
|- ( F ~~> A -> E! x F ~~> x )

Proof

Step Hyp Ref Expression
1 climcl 
 |-  ( F ~~> A -> A e. CC )
2 breq2 
 |-  ( y = A -> ( F ~~> y <-> F ~~> A ) )
3 2 spcegv 
 |-  ( A e. CC -> ( F ~~> A -> E. y F ~~> y ) )
4 1 3 mpcom 
 |-  ( F ~~> A -> E. y F ~~> y )
5 climuni 
 |-  ( ( F ~~> y /\ F ~~> x ) -> y = x )
6 5 gen2 
 |-  A. y A. x ( ( F ~~> y /\ F ~~> x ) -> y = x )
7 nfv 
 |-  F/ y F ~~> x
8 nfv 
 |-  F/ x F ~~> y
9 breq2 
 |-  ( x = y -> ( F ~~> x <-> F ~~> y ) )
10 7 8 9 cbveuw 
 |-  ( E! x F ~~> x <-> E! y F ~~> y )
11 breq2 
 |-  ( y = x -> ( F ~~> y <-> F ~~> x ) )
12 11 eu4 
 |-  ( E! y F ~~> y <-> ( E. y F ~~> y /\ A. y A. x ( ( F ~~> y /\ F ~~> x ) -> y = x ) ) )
13 10 12 bitri 
 |-  ( E! x F ~~> x <-> ( E. y F ~~> y /\ A. y A. x ( ( F ~~> y /\ F ~~> x ) -> y = x ) ) )
14 4 6 13 sylanblrc 
 |-  ( F ~~> A -> E! x F ~~> x )