Metamath Proof Explorer

Theorem fclim

Description: The limit relation is function-like, and with codomain the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion fclim 
|- ~~> : dom ~~> --> CC

Proof

Step Hyp Ref Expression
1 climrel 
 |-  Rel ~~>
2 climuni 
 |-  ( ( x ~~> y /\ x ~~> z ) -> y = z )
3 2 ax-gen 
 |-  A. z ( ( x ~~> y /\ x ~~> z ) -> y = z )
4 3 ax-gen 
 |-  A. y A. z ( ( x ~~> y /\ x ~~> z ) -> y = z )
5 4 ax-gen 
 |-  A. x A. y A. z ( ( x ~~> y /\ x ~~> z ) -> y = z )
6 dffun2 
 |-  ( Fun ~~> <-> ( Rel ~~> /\ A. x A. y A. z ( ( x ~~> y /\ x ~~> z ) -> y = z ) ) )
7 1 5 6 mpbir2an 
 |-  Fun ~~>
8 funfn 
 |-  ( Fun ~~> <-> ~~> Fn dom ~~> )
9 7 8 mpbi 
 |-  ~~> Fn dom ~~>
10 vex 
 |-  y e. _V
11 10 elrn 
 |-  ( y e. ran ~~> <-> E. x x ~~> y )
12 climcl 
 |-  ( x ~~> y -> y e. CC )
13 12 exlimiv 
 |-  ( E. x x ~~> y -> y e. CC )
14 11 13 sylbi 
 |-  ( y e. ran ~~> -> y e. CC )
15 14 ssriv 
 |-  ran ~~> C_ CC
16 df-f 
 |-  ( ~~> : dom ~~> --> CC <-> ( ~~> Fn dom ~~> /\ ran ~~> C_ CC ) )
17 9 15 16 mpbir2an 
 |-  ~~> : dom ~~> --> CC