Metamath Proof Explorer

Theorem cnlimc

Description: F is a continuous function iff the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion cnlimc 
|- ( A C_ CC -> ( F e. ( A -cn-> CC ) <-> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F limCC x ) ) ) )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  CC C_ CC
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t A ) = ( ( TopOpen ` CCfld ) |`t A )
4 2 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
5 4 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
6 2 3 5 cncfcn 
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( A -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
7 1 6 mpan2 
 |-  ( A C_ CC -> ( A -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
8 7 eleq2d 
 |-  ( A C_ CC -> ( F e. ( A -cn-> CC ) <-> F e. ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) ) )
9 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ A C_ CC ) -> ( ( TopOpen ` CCfld ) |`t A ) e. ( TopOn ` A ) )
10 4 9 mpan 
 |-  ( A C_ CC -> ( ( TopOpen ` CCfld ) |`t A ) e. ( TopOn ` A ) )
11 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t A ) e. ( TopOn ` A ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( F e. ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) <-> ( F : A --> CC /\ A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) ) ) )
12 10 4 11 sylancl 
 |-  ( A C_ CC -> ( F e. ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) <-> ( F : A --> CC /\ A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) ) ) )
13 2 3 cnplimc 
 |-  ( ( A C_ CC /\ x e. A ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> ( F : A --> CC /\ ( F ` x ) e. ( F limCC x ) ) ) )
14 13 baibd 
 |-  ( ( ( A C_ CC /\ x e. A ) /\ F : A --> CC ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> ( F ` x ) e. ( F limCC x ) ) )
15 14 an32s 
 |-  ( ( ( A C_ CC /\ F : A --> CC ) /\ x e. A ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> ( F ` x ) e. ( F limCC x ) ) )
16 15 ralbidva 
 |-  ( ( A C_ CC /\ F : A --> CC ) -> ( A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> A. x e. A ( F ` x ) e. ( F limCC x ) ) )
17 16 pm5.32da 
 |-  ( A C_ CC -> ( ( F : A --> CC /\ A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) ) <-> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F limCC x ) ) ) )
18 8 12 17 3bitrd 
 |-  ( A C_ CC -> ( F e. ( A -cn-> CC ) <-> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F limCC x ) ) ) )