Metamath Proof Explorer

Theorem ellimc

Description: Value of the limit predicate. C is the limit of the function F at B if the function G , formed by adding B to the domain of F and setting it to C , is continuous at B . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcval.j ⊢ J = K ↾ 𝑡 A ∪ B
limcval.k ⊢ K = TopOpen ⁡ ℂ fld
ellimc.g ⊢ G = z ∈ A ∪ B ⟼ if z = B C F ⁡ z
ellimc.f ⊢ φ → F : A ⟶ ℂ
ellimc.a ⊢ φ → A ⊆ ℂ
ellimc.b ⊢ φ → B ∈ ℂ
Assertion ellimc ⊢ φ → C ∈ F lim ℂ B ↔ G ∈ J CnP K ⁡ B

Proof

Step Hyp Ref Expression
1 limcval.j ⊢ J = K ↾ 𝑡 A ∪ B
2 limcval.k ⊢ K = TopOpen ⁡ ℂ fld
3 ellimc.g ⊢ G = z ∈ A ∪ B ⟼ if z = B C F ⁡ z
4 ellimc.f ⊢ φ → F : A ⟶ ℂ
5 ellimc.a ⊢ φ → A ⊆ ℂ
6 ellimc.b ⊢ φ → B ∈ ℂ
7 1 2 limcfval ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ → F lim ℂ B = y | z ∈ A ∪ B ⟼ if z = B y F ⁡ z ∈ J CnP K ⁡ B ∧ F lim ℂ B ⊆ ℂ
8 4 5 6 7 syl3anc ⊢ φ → F lim ℂ B = y | z ∈ A ∪ B ⟼ if z = B y F ⁡ z ∈ J CnP K ⁡ B ∧ F lim ℂ B ⊆ ℂ
9 8 simpld ⊢ φ → F lim ℂ B = y | z ∈ A ∪ B ⟼ if z = B y F ⁡ z ∈ J CnP K ⁡ B
10 9 eleq2d ⊢ φ → C ∈ F lim ℂ B ↔ C ∈ y | z ∈ A ∪ B ⟼ if z = B y F ⁡ z ∈ J CnP K ⁡ B
11 1 2 3 limcvallem ⊢ F : A ⟶ ℂ ∧ A ⊆ ℂ ∧ B ∈ ℂ → G ∈ J CnP K ⁡ B → C ∈ ℂ
12 4 5 6 11 syl3anc ⊢ φ → G ∈ J CnP K ⁡ B → C ∈ ℂ
13 ifeq1 ⊢ y = C → if z = B y F ⁡ z = if z = B C F ⁡ z
14 13 mpteq2dv ⊢ y = C → z ∈ A ∪ B ⟼ if z = B y F ⁡ z = z ∈ A ∪ B ⟼ if z = B C F ⁡ z
15 14 3 eqtr4di ⊢ y = C → z ∈ A ∪ B ⟼ if z = B y F ⁡ z = G
16 15 eleq1d ⊢ y = C → z ∈ A ∪ B ⟼ if z = B y F ⁡ z ∈ J CnP K ⁡ B ↔ G ∈ J CnP K ⁡ B
17 16 elab3g ⊢ G ∈ J CnP K ⁡ B → C ∈ ℂ → C ∈ y | z ∈ A ∪ B ⟼ if z = B y F ⁡ z ∈ J CnP K ⁡ B ↔ G ∈ J CnP K ⁡ B
18 12 17 syl ⊢ φ → C ∈ y | z ∈ A ∪ B ⟼ if z = B y F ⁡ z ∈ J CnP K ⁡ B ↔ G ∈ J CnP K ⁡ B
19 10 18 bitrd ⊢ φ → C ∈ F lim ℂ B ↔ G ∈ J CnP K ⁡ B