Definition df-limc 22798

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 22794	. 2 class lim CC
2		vf	. . 3 setvar f
3		vx	. . 3 setvar x
4		cc 9533	. . . 4 class CC
5		cpm 7473	. . . 4 class ^pm
6	4, 4, 5	co 6297	. . 3 class ( CC ^pm CC )
7		vz	. . . . . . 7 setvar z
8	2	cv 1436	. . . . . . . . 9 class f
9	8	cdm 4846	. . . . . . . 8 class dom f
10	3	cv 1436	. . . . . . . . 9 class x
11	10	csn 3993	. . . . . . . 8 class { x }
12	9, 11	cun 3431	. . . . . . 7 class ( dom f u. { x } )
13	7, 3	weq 1780	. . . . . . . 8 wff z = x
14		vy	. . . . . . . . 9 setvar y
15	14	cv 1436	. . . . . . . 8 class y
16	7	cv 1436	. . . . . . . . 9 class z
17	16, 8	cfv 5593	. . . . . . . 8 class ( f ` z )
18	13, 15, 17	cif 3906	. . . . . . 7 class if ( z = x , y , ( f ` z ) )
19	7, 12, 18	cmpt 4476	. . . . . 6 class ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) )
20		vj	. . . . . . . . . 10 setvar j
21	20	cv 1436	. . . . . . . . 9 class j
22		crest 15297	. . . . . . . . 9 class ↾t
23	21, 12, 22	co 6297	. . . . . . . 8 class ( j ↾t ( dom f u. { x } ) )
24		ccnp 20218	. . . . . . . 8 class CnP
25	23, 21, 24	co 6297	. . . . . . 7 class ( ( j ↾t ( dom f u. { x } ) ) CnP j )
26	10, 25	cfv 5593	. . . . . 6 class ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x )
27	19, 26	wcel 1867	. . . . 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 18948	. . . . . 6 class ℂfld
29		ctopn 15298	. . . . . 6 class TopOpen
30	28, 29	cfv 5593	. . . . 5 class ( TopOpen ` ℂfld )
31	27, 20, 30	wsbc 3296	. . . 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 2405	. . 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 6299	. 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 1437	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  22804  limcrcl  22806