Definition df-limc 19706

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.)

Assertion

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

Distinct variable group:   f, j, x, y, z

Detailed syntax breakdown of Definition df-limc

Step	Hyp	Ref	Expression
1		climc 19702	. 2 class lim CC
2		vf	. . 3 set f
3		vx	. . 3 set x
4		cc 8944	. . . 4 class CC
5		cpm 6978	. . . 4 class ^pm
6	4, 4, 5	co 6040	. . 3 class ( CC ^pm CC )
7		vz	. . . . . . 7 set z
8	2	cv 1648	. . . . . . . . 9 class f
9	8	cdm 4837	. . . . . . . 8 class dom f
10	3	cv 1648	. . . . . . . . 9 class x
11	10	csn 3774	. . . . . . . 8 class { x }
12	9, 11	cun 3278	. . . . . . 7 class ( dom f u. { x } )
13	7, 3	weq 1650	. . . . . . . 8 wff z = x
14		vy	. . . . . . . . 9 set y
15	14	cv 1648	. . . . . . . 8 class y
16	7	cv 1648	. . . . . . . . 9 class z
17	16, 8	cfv 5413	. . . . . . . 8 class ( f ` z )
18	13, 15, 17	cif 3699	. . . . . . 7 class if ( z = x , y , ( f ` z ) )
19	7, 12, 18	cmpt 4226	. . . . . 6 class ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) )
20		vj	. . . . . . . . . 10 set j
21	20	cv 1648	. . . . . . . . 9 class j
22		crest 13603	. . . . . . . . 9 class ↾t
23	21, 12, 22	co 6040	. . . . . . . 8 class ( j ↾t ( dom f u. { x } ) )
24		ccnp 17243	. . . . . . . 8 class CnP
25	23, 21, 24	co 6040	. . . . . . 7 class ( ( j ↾t ( dom f u. { x } ) ) CnP j )
26	10, 25	cfv 5413	. . . . . 6 class ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x )
27	19, 26	wcel 1721	. . . . 5 wff ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x )
28		ccnfld 16658	. . . . . 6 class ℂfld
29		ctopn 13604	. . . . . 6 class TopOpen
30	28, 29	cfv 5413	. . . . 5 class ( TopOpen ` ℂfld )
31	27, 20, 30	wsbc 3121	. . . 4 wff [. ( TopOpen ` ℂfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x )
32	31, 14	cab 2390	. . 3 class { y | [. ( TopOpen ` ℂfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x ) }
33	2, 3, 6, 4, 32	cmpt2 6042	. 2 class ( f e. ( CC ^pm CC ) , x e. CC |-> { y | [. ( TopOpen ` ℂfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x ) } )
34	1, 33	wceq 1649	1 wff lim CC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y | [. ( TopOpen ` ℂfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x ) } )

This definition is referenced by:  limcfval  19712  limcrcl  19714