Metamath Proof Explorer

Theorem cnplimc

Description: A function is continuous at B iff its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses cnplimc.k 
|- K = ( TopOpen ` CCfld )
cnplimc.j 
|- J = ( K |`t A )
Assertion cnplimc 
|- ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )

Proof

Step Hyp Ref Expression
1 cnplimc.k 
 |-  K = ( TopOpen ` CCfld )
2 cnplimc.j 
 |-  J = ( K |`t A )
3 1 cnfldtopon 
 |-  K e. ( TopOn ` CC )
4 simpl 
 |-  ( ( A C_ CC /\ B e. A ) -> A C_ CC )
5 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ A C_ CC ) -> ( K |`t A ) e. ( TopOn ` A ) )
6 3 4 5 sylancr 
 |-  ( ( A C_ CC /\ B e. A ) -> ( K |`t A ) e. ( TopOn ` A ) )
7 2 6 eqeltrid 
 |-  ( ( A C_ CC /\ B e. A ) -> J e. ( TopOn ` A ) )
8 cnpf2 
 |-  ( ( J e. ( TopOn ` A ) /\ K e. ( TopOn ` CC ) /\ F e. ( ( J CnP K ) ` B ) ) -> F : A --> CC )
9 8 3expia 
 |-  ( ( J e. ( TopOn ` A ) /\ K e. ( TopOn ` CC ) ) -> ( F e. ( ( J CnP K ) ` B ) -> F : A --> CC ) )
10 7 3 9 sylancl 
 |-  ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) -> F : A --> CC ) )
11 10 pm4.71rd 
 |-  ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ F e. ( ( J CnP K ) ` B ) ) ) )
12 simpr 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> F : A --> CC )
13 simplr 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> B e. A )
14 13 snssd 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> { B } C_ A )
15 ssequn2 
 |-  ( { B } C_ A <-> ( A u. { B } ) = A )
16 14 15 sylib 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( A u. { B } ) = A )
17 16 feq2d 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( F : ( A u. { B } ) --> CC <-> F : A --> CC ) )
18 12 17 mpbird 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> F : ( A u. { B } ) --> CC )
19 18 feqmptd 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> F = ( x e. ( A u. { B } ) |-> ( F ` x ) ) )
20 16 oveq2d 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( K |`t ( A u. { B } ) ) = ( K |`t A ) )
21 2 20 eqtr4id 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> J = ( K |`t ( A u. { B } ) ) )
22 21 oveq1d 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( J CnP K ) = ( ( K |`t ( A u. { B } ) ) CnP K ) )
23 22 fveq1d 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( ( J CnP K ) ` B ) = ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) )
24 19 23 eleq12d 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( x e. ( A u. { B } ) |-> ( F ` x ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
25 eqid 
 |-  ( K |`t ( A u. { B } ) ) = ( K |`t ( A u. { B } ) )
26 ifid 
 |-  if ( x = B , ( F ` x ) , ( F ` x ) ) = ( F ` x )
27 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
28 27 adantl 
 |-  ( ( x e. ( A u. { B } ) /\ x = B ) -> ( F ` x ) = ( F ` B ) )
29 28 ifeq1da 
 |-  ( x e. ( A u. { B } ) -> if ( x = B , ( F ` x ) , ( F ` x ) ) = if ( x = B , ( F ` B ) , ( F ` x ) ) )
30 26 29 eqtr3id 
 |-  ( x e. ( A u. { B } ) -> ( F ` x ) = if ( x = B , ( F ` B ) , ( F ` x ) ) )
31 30 mpteq2ia 
 |-  ( x e. ( A u. { B } ) |-> ( F ` x ) ) = ( x e. ( A u. { B } ) |-> if ( x = B , ( F ` B ) , ( F ` x ) ) )
32 simpll 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> A C_ CC )
33 32 13 sseldd 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> B e. CC )
34 25 1 31 12 32 33 ellimc 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( ( F ` B ) e. ( F limCC B ) <-> ( x e. ( A u. { B } ) |-> ( F ` x ) ) e. ( ( ( K |`t ( A u. { B } ) ) CnP K ) ` B ) ) )
35 24 34 bitr4d 
 |-  ( ( ( A C_ CC /\ B e. A ) /\ F : A --> CC ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F ` B ) e. ( F limCC B ) ) )
36 35 pm5.32da 
 |-  ( ( A C_ CC /\ B e. A ) -> ( ( F : A --> CC /\ F e. ( ( J CnP K ) ` B ) ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )
37 11 36 bitrd 
 |-  ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )