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	$$⊢{lim}_{ℂ}=\left(f\in \left(ℂ{\uparrow }_{𝑝𝑚}ℂ\right),x\in ℂ⟼\left\{y|\underset{\dot{}}{[}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)/j\underset{\dot{}}{]}\left(z\in \left(\mathrm{dom}f\cup \left\{x\right\}\right)⟼if\left(z=x,y,f\left(z\right)\right)\right)\in \left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)\left(x\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		climc	$$class{lim}_{ℂ}$$
1		vf	$$setvarf$$
2		cc	$$classℂ$$
3		cpm	$$class{\uparrow }_{𝑝𝑚}$$
4	2 2 3	co	$$class\left(ℂ{\uparrow }_{𝑝𝑚}ℂ\right)$$
5		vx	$$setvarx$$
6		vy	$$setvary$$
7		ctopn	$$class\mathrm{TopOpen}$$
8		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
9	8 7	cfv	$$class\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
10		vj	$$setvarj$$
11		vz	$$setvarz$$
12	1	cv	$$setvarf$$
13	12	cdm	$$class\mathrm{dom}f$$
14	5	cv	$$setvarx$$
15	14	csn	$$class\left\{x\right\}$$
16	13 15	cun	$$class\left(\mathrm{dom}f\cup \left\{x\right\}\right)$$
17	11	cv	$$setvarz$$
18	17 14	wceq	$$wffz=x$$
19	6	cv	$$setvary$$
20	17 12	cfv	$$classf\left(z\right)$$
21	18 19 20	cif	$$classif\left(z=x,y,f\left(z\right)\right)$$
22	11 16 21	cmpt	$$class\left(z\in \left(\mathrm{dom}f\cup \left\{x\right\}\right)⟼if\left(z=x,y,f\left(z\right)\right)\right)$$
23	10	cv	$$setvarj$$
24		crest	$$class{\upharpoonright }_{𝑡}$$
25	23 16 24	co	$$class\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)$$
26		ccnp	$$class\mathrm{CnP}$$
27	25 23 26	co	$$class\left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)$$
28	14 27	cfv	$$class\left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)\left(x\right)$$
29	22 28	wcel	$$wff\left(z\in \left(\mathrm{dom}f\cup \left\{x\right\}\right)⟼if\left(z=x,y,f\left(z\right)\right)\right)\in \left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)\left(x\right)$$
30	29 10 9	wsbc	$$wff\underset{\dot{}}{[}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)/j\underset{\dot{}}{]}\left(z\in \left(\mathrm{dom}f\cup \left\{x\right\}\right)⟼if\left(z=x,y,f\left(z\right)\right)\right)\in \left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)\left(x\right)$$
31	30 6	cab	$$class\left\{y|\underset{\dot{}}{[}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)/j\underset{\dot{}}{]}\left(z\in \left(\mathrm{dom}f\cup \left\{x\right\}\right)⟼if\left(z=x,y,f\left(z\right)\right)\right)\in \left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)\left(x\right)\right\}$$
32	1 5 4 2 31	cmpo	$$class\left(f\in \left(ℂ{\uparrow }_{𝑝𝑚}ℂ\right),x\in ℂ⟼\left\{y|\underset{\dot{}}{[}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)/j\underset{\dot{}}{]}\left(z\in \left(\mathrm{dom}f\cup \left\{x\right\}\right)⟼if\left(z=x,y,f\left(z\right)\right)\right)\in \left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)\left(x\right)\right\}\right)$$
33	0 32	wceq	$$wff{lim}_{ℂ}=\left(f\in \left(ℂ{\uparrow }_{𝑝𝑚}ℂ\right),x\in ℂ⟼\left\{y|\underset{\dot{}}{[}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)/j\underset{\dot{}}{]}\left(z\in \left(\mathrm{dom}f\cup \left\{x\right\}\right)⟼if\left(z=x,y,f\left(z\right)\right)\right)\in \left(\left(j{\upharpoonright }_{𝑡}\left(\mathrm{dom}f\cup \left\{x\right\}\right)\right)\mathrm{CnP}j\right)\left(x\right)\right\}\right)$$