Metamath Proof Explorer

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 ℂ = f ∈ ℂ ↑ 𝑝𝑚 ℂ , x ∈ ℂ ⟼ y | [˙ TopOpen ⁡ ℂ fld / j]˙ z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z ∈ j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 climc class lim ℂ
1 vf setvar f
2 cc class ℂ
3 cpm class ↑ 𝑝𝑚
4 2 2 3 co class ℂ ↑ 𝑝𝑚 ℂ
5 vx setvar x
6 vy setvar y
7 ctopn class TopOpen
8 ccnfld class ℂ fld
9 8 7 cfv class TopOpen ⁡ ℂ fld
10 vj setvar j
11 vz setvar z
12 1 cv setvar f
13 12 cdm class dom ⁡ f
14 5 cv setvar x
15 14 csn class x
16 13 15 cun class dom ⁡ f ∪ x
17 11 cv setvar z
18 17 14 wceq wff z = x
19 6 cv setvar y
20 17 12 cfv class f ⁡ z
21 18 19 20 cif class if z = x y f ⁡ z
22 11 16 21 cmpt class z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z
23 10 cv setvar j
24 crest class ↾ 𝑡
25 23 16 24 co class j ↾ 𝑡 dom ⁡ f ∪ x
26 ccnp class CnP
27 25 23 26 co class j ↾ 𝑡 dom ⁡ f ∪ x CnP j
28 14 27 cfv class j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x
29 22 28 wcel wff z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z ∈ j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x
30 29 10 9 wsbc wff [˙ TopOpen ⁡ ℂ fld / j]˙ z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z ∈ j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x
31 30 6 cab class y | [˙ TopOpen ⁡ ℂ fld / j]˙ z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z ∈ j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x
32 1 5 4 2 31 cmpo class f ∈ ℂ ↑ 𝑝𝑚 ℂ , x ∈ ℂ ⟼ y | [˙ TopOpen ⁡ ℂ fld / j]˙ z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z ∈ j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x
33 0 32 wceq wff lim ℂ = f ∈ ℂ ↑ 𝑝𝑚 ℂ , x ∈ ℂ ⟼ y | [˙ TopOpen ⁡ ℂ fld / j]˙ z ∈ dom ⁡ f ∪ x ⟼ if z = x y f ⁡ z ∈ j ↾ 𝑡 dom ⁡ f ∪ x CnP j ⁡ x