Definition df-limc 24935

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ℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∣ [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})

Distinct variable group:   𝑓,𝑗,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-limc

Step	Hyp	Ref	Expression
1		climc 24931	. 2 class limℂ
2		vf	. . 3 setvar 𝑓
3		vx	. . 3 setvar 𝑥
4		cc 10800	. . . 4 class ℂ
5		cpm 8574	. . . 4 class ↑pm
6	4, 4, 5	co 7255	. . 3 class (ℂ ↑pm ℂ)
7		vz	. . . . . . 7 setvar 𝑧
8	2	cv 1538	. . . . . . . . 9 class 𝑓
9	8	cdm 5580	. . . . . . . 8 class dom 𝑓
10	3	cv 1538	. . . . . . . . 9 class 𝑥
11	10	csn 4558	. . . . . . . 8 class {𝑥}
12	9, 11	cun 3881	. . . . . . 7 class (dom 𝑓 ∪ {𝑥})
13	7, 3	weq 1967	. . . . . . . 8 wff 𝑧 = 𝑥
14		vy	. . . . . . . . 9 setvar 𝑦
15	14	cv 1538	. . . . . . . 8 class 𝑦
16	7	cv 1538	. . . . . . . . 9 class 𝑧
17	16, 8	cfv 6418	. . . . . . . 8 class (𝑓‘𝑧)
18	13, 15, 17	cif 4456	. . . . . . 7 class if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))
19	7, 12, 18	cmpt 5153	. . . . . 6 class (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧)))
20		vj	. . . . . . . . . 10 setvar 𝑗
21	20	cv 1538	. . . . . . . . 9 class 𝑗
22		crest 17048	. . . . . . . . 9 class ↾t
23	21, 12, 22	co 7255	. . . . . . . 8 class (𝑗 ↾t (dom 𝑓 ∪ {𝑥}))
24		ccnp 22284	. . . . . . . 8 class CnP
25	23, 21, 24	co 7255	. . . . . . 7 class ((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)
26	10, 25	cfv 6418	. . . . . 6 class (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
27	19, 26	wcel 2108	. . . . 5 wff (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
28		ccnfld 20510	. . . . . 6 class ℂfld
29		ctopn 17049	. . . . . 6 class TopOpen
30	28, 29	cfv 6418	. . . . 5 class (TopOpen‘ℂfld)
31	27, 20, 30	wsbc 3711	. . . 4 wff [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
32	31, 14	cab 2715	. . 3 class {𝑦 ∣ [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}
33	2, 3, 6, 4, 32	cmpo 7257	. 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∣ [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
34	1, 33	wceq 1539	1 wff limℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∣ [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})

This definition is referenced by:  limcfval  24941  limcrcl  24943