Definition df-limced 13419

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.) (Revised by Jim Kingdon, 3-Jun-2023.)

Assertion

Ref	Expression
df-limced	⊢ limℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))})

Distinct variable group:   𝑒,𝑑,𝑓,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-limced

Step	Hyp	Ref	Expression
1		climc 13417	. 2 class limℂ
2		vf	. . 3 setvar 𝑓
3		vx	. . 3 setvar 𝑥
4		cc 7772	. . . 4 class ℂ
5		cpm 6627	. . . 4 class ↑pm
6	4, 4, 5	co 5853	. . 3 class (ℂ ↑pm ℂ)
7	2	cv 1347	. . . . . . . 8 class 𝑓
8	7	cdm 4611	. . . . . . 7 class dom 𝑓
9	8, 4, 7	wf 5194	. . . . . 6 wff 𝑓:dom 𝑓⟶ℂ
10	8, 4	wss 3121	. . . . . 6 wff dom 𝑓 ⊆ ℂ
11	9, 10	wa 103	. . . . 5 wff (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ)
12	3	cv 1347	. . . . . . 7 class 𝑥
13	12, 4	wcel 2141	. . . . . 6 wff 𝑥 ∈ ℂ
14		vz	. . . . . . . . . . . . 13 setvar 𝑧
15	14	cv 1347	. . . . . . . . . . . 12 class 𝑧
16		cap 8500	. . . . . . . . . . . 12 class #
17	15, 12, 16	wbr 3989	. . . . . . . . . . 11 wff 𝑧 # 𝑥
18		cmin 8090	. . . . . . . . . . . . . 14 class −
19	15, 12, 18	co 5853	. . . . . . . . . . . . 13 class (𝑧 − 𝑥)
20		cabs 10961	. . . . . . . . . . . . 13 class abs
21	19, 20	cfv 5198	. . . . . . . . . . . 12 class (abs‘(𝑧 − 𝑥))
22		vd	. . . . . . . . . . . . 13 setvar 𝑑
23	22	cv 1347	. . . . . . . . . . . 12 class 𝑑
24		clt 7954	. . . . . . . . . . . 12 class <
25	21, 23, 24	wbr 3989	. . . . . . . . . . 11 wff (abs‘(𝑧 − 𝑥)) < 𝑑
26	17, 25	wa 103	. . . . . . . . . 10 wff (𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑)
27	15, 7	cfv 5198	. . . . . . . . . . . . 13 class (𝑓‘𝑧)
28		vy	. . . . . . . . . . . . . 14 setvar 𝑦
29	28	cv 1347	. . . . . . . . . . . . 13 class 𝑦
30	27, 29, 18	co 5853	. . . . . . . . . . . 12 class ((𝑓‘𝑧) − 𝑦)
31	30, 20	cfv 5198	. . . . . . . . . . 11 class (abs‘((𝑓‘𝑧) − 𝑦))
32		ve	. . . . . . . . . . . 12 setvar 𝑒
33	32	cv 1347	. . . . . . . . . . 11 class 𝑒
34	31, 33, 24	wbr 3989	. . . . . . . . . 10 wff (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒
35	26, 34	wi 4	. . . . . . . . 9 wff ((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)
36	35, 14, 8	wral 2448	. . . . . . . 8 wff ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)
37		crp 9610	. . . . . . . 8 class ℝ+
38	36, 22, 37	wrex 2449	. . . . . . 7 wff ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)
39	38, 32, 37	wral 2448	. . . . . 6 wff ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)
40	13, 39	wa 103	. . . . 5 wff (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒))
41	11, 40	wa 103	. . . 4 wff ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))
42	41, 28, 4	crab 2452	. . 3 class {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))}
43	2, 3, 6, 4, 42	cmpo 5855	. 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))})
44	1, 43	wceq 1348	1 wff limℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧 − 𝑥)) < 𝑑) → (abs‘((𝑓‘𝑧) − 𝑦)) < 𝑒)))})

This definition is referenced by:  limcrcl  13421  limccl  13422  ellimc3apf  13423