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𝑡AB
limcval.k K=TopOpenfld
ellimc.g G=zABifz=BCFz
ellimc.f φF:A
ellimc.a φA
ellimc.b φB
Assertion ellimc φCFlimBGJCnPKB

Proof

Step Hyp Ref Expression
1 limcval.j J=K𝑡AB
2 limcval.k K=TopOpenfld
3 ellimc.g G=zABifz=BCFz
4 ellimc.f φF:A
5 ellimc.a φA
6 ellimc.b φB
7 1 2 limcfval F:AABFlimB=y|zABifz=ByFzJCnPKBFlimB
8 4 5 6 7 syl3anc φFlimB=y|zABifz=ByFzJCnPKBFlimB
9 8 simpld φFlimB=y|zABifz=ByFzJCnPKB
10 9 eleq2d φCFlimBCy|zABifz=ByFzJCnPKB
11 1 2 3 limcvallem F:AABGJCnPKBC
12 4 5 6 11 syl3anc φGJCnPKBC
13 ifeq1 y=Cifz=ByFz=ifz=BCFz
14 13 mpteq2dv y=CzABifz=ByFz=zABifz=BCFz
15 14 3 eqtr4di y=CzABifz=ByFz=G
16 15 eleq1d y=CzABifz=ByFzJCnPKBGJCnPKB
17 16 elab3g GJCnPKBCCy|zABifz=ByFzJCnPKBGJCnPKB
18 12 17 syl φCy|zABifz=ByFzJCnPKBGJCnPKB
19 10 18 bitrd φCFlimBGJCnPKB