Definition df-limc 22560

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 22556	. 2 class lim CC
2		vf	. . 3 setvar f
3		vx	. . 3 setvar x
4		cc 9519	. . . 4 class CC
5		cpm 7457	. . . 4 class ^pm
6	4, 4, 5	co 6277	. . 3 class ( CC ^pm CC )
7		vz	. . . . . . 7 setvar z
8	2	cv 1404	. . . . . . . . 9 class f
9	8	cdm 4822	. . . . . . . 8 class dom f
10	3	cv 1404	. . . . . . . . 9 class x
11	10	csn 3971	. . . . . . . 8 class { x }
12	9, 11	cun 3411	. . . . . . 7 class ( dom f u. { x } )
13	7, 3	weq 1757	. . . . . . . 8 wff z = x
14		vy	. . . . . . . . 9 setvar y
15	14	cv 1404	. . . . . . . 8 class y
16	7	cv 1404	. . . . . . . . 9 class z
17	16, 8	cfv 5568	. . . . . . . 8 class ( f ` z )
18	13, 15, 17	cif 3884	. . . . . . 7 class if ( z = x , y , ( f ` z ) )
19	7, 12, 18	cmpt 4452	. . . . . 6 class ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) )
20		vj	. . . . . . . . . 10 setvar j
21	20	cv 1404	. . . . . . . . 9 class j
22		crest 15033	. . . . . . . . 9 class ↾t
23	21, 12, 22	co 6277	. . . . . . . 8 class ( j ↾t ( dom f u. { x } ) )
24		ccnp 20017	. . . . . . . 8 class CnP
25	23, 21, 24	co 6277	. . . . . . 7 class ( ( j ↾t ( dom f u. { x } ) ) CnP j )
26	10, 25	cfv 5568	. . . . . 6 class ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x )
27	19, 26	wcel 1842	. . . . 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 18738	. . . . . 6 class ℂfld
29		ctopn 15034	. . . . . 6 class TopOpen
30	28, 29	cfv 5568	. . . . 5 class ( TopOpen ` ℂfld )
31	27, 20, 30	wsbc 3276	. . . 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 2387	. . 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 6279	. 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 1405	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  22566  limcrcl  22568