Metamath Proof Explorer

Definition df-limc

Description: Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion df-limc 
|- limCC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y | [. ( TopOpen ` CCfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 climc 
 |-  limCC
1 vf 
 |-  f
2 cc 
 |-  CC
3 cpm 
 |-  ^pm
4 2 2 3 co 
 |-  ( CC ^pm CC )
5 vx 
 |-  x
6 vy 
 |-  y
7 ctopn 
 |-  TopOpen
8 ccnfld 
 |-  CCfld
9 8 7 cfv 
 |-  ( TopOpen ` CCfld )
10 vj 
 |-  j
11 vz 
 |-  z
12 1 cv 
 |-  f
13 12 cdm 
 |-  dom f
14 5 cv 
 |-  x
15 14 csn 
 |-  { x }
16 13 15 cun 
 |-  ( dom f u. { x } )
17 11 cv 
 |-  z
18 17 14 wceq 
 |-  z = x
19 6 cv 
 |-  y
20 17 12 cfv 
 |-  ( f ` z )
21 18 19 20 cif 
 |-  if ( z = x , y , ( f ` z ) )
22 11 16 21 cmpt 
 |-  ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) )
23 10 cv 
 |-  j
24 crest 
 |-  |`t
25 23 16 24 co 
 |-  ( j |`t ( dom f u. { x } ) )
26 ccnp 
 |-  CnP
27 25 23 26 co 
 |-  ( ( j |`t ( dom f u. { x } ) ) CnP j )
28 14 27 cfv 
 |-  ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x )
29 22 28 wcel 
 |-  ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x )
30 29 10 9 wsbc 
 |-  [. ( TopOpen ` CCfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x )
31 30 6 cab 
 |-  { y | [. ( TopOpen ` CCfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) }
32 1 5 4 2 31 cmpo 
 |-  ( f e. ( CC ^pm CC ) , x e. CC |-> { y | [. ( TopOpen ` CCfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) } )
33 0 32 wceq 
 |-  limCC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y | [. ( TopOpen ` CCfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) } )