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