Definition df-limc 22021

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 22017	. 2 class lim CC
2		vf	. . 3 setvar f
3		vx	. . 3 setvar x
4		cc 9489	. . . 4 class CC
5		cpm 7421	. . . 4 class ^pm
6	4, 4, 5	co 6283	. . 3 class ( CC ^pm CC )
7		vz	. . . . . . 7 setvar z
8	2	cv 1378	. . . . . . . . 9 class f
9	8	cdm 4999	. . . . . . . 8 class dom f
10	3	cv 1378	. . . . . . . . 9 class x
11	10	csn 4027	. . . . . . . 8 class { x }
12	9, 11	cun 3474	. . . . . . 7 class ( dom f u. { x } )
13	7, 3	weq 1705	. . . . . . . 8 wff z = x
14		vy	. . . . . . . . 9 setvar y
15	14	cv 1378	. . . . . . . 8 class y
16	7	cv 1378	. . . . . . . . 9 class z
17	16, 8	cfv 5587	. . . . . . . 8 class ( f ` z )
18	13, 15, 17	cif 3939	. . . . . . 7 class if ( z = x , y , ( f ` z ) )
19	7, 12, 18	cmpt 4505	. . . . . 6 class ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) )
20		vj	. . . . . . . . . 10 setvar j
21	20	cv 1378	. . . . . . . . 9 class j
22		crest 14675	. . . . . . . . 9 class ↾t
23	21, 12, 22	co 6283	. . . . . . . 8 class ( j ↾t ( dom f u. { x } ) )
24		ccnp 19508	. . . . . . . 8 class CnP
25	23, 21, 24	co 6283	. . . . . . 7 class ( ( j ↾t ( dom f u. { x } ) ) CnP j )
26	10, 25	cfv 5587	. . . . . 6 class ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x )
27	19, 26	wcel 1767	. . . . 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 18207	. . . . . 6 class ℂfld
29		ctopn 14676	. . . . . 6 class TopOpen
30	28, 29	cfv 5587	. . . . 5 class ( TopOpen ` ℂfld )
31	27, 20, 30	wsbc 3331	. . . 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 2452	. . 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 6285	. 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 1379	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  22027  limcrcl  22029