Metamath Proof Explorer

Theorem dvcn

Description: A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-Sep-2015)

Ref Expression
Assertion dvcn 
|- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> F e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> F : A --> CC )
2 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t A ) = ( ( TopOpen ` CCfld ) |`t A )
3 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 2 3 dvcnp2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ x e. dom ( S _D F ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) )
5 4 ralrimiva 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> A. x e. dom ( S _D F ) F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) )
6 raleq 
 |-  ( dom ( S _D F ) = A -> ( A. x e. dom ( S _D F ) F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) ) )
7 6 biimpd 
 |-  ( dom ( S _D F ) = A -> ( A. x e. dom ( S _D F ) F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) -> A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) ) )
8 5 7 mpan9 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) )
9 3 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
10 simpl3 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> A C_ S )
11 simpl1 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> S C_ CC )
12 10 11 sstrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> A C_ CC )
13 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ A C_ CC ) -> ( ( TopOpen ` CCfld ) |`t A ) e. ( TopOn ` A ) )
14 9 12 13 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> ( ( TopOpen ` CCfld ) |`t A ) e. ( TopOn ` A ) )
15 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 ) ) ) )
16 14 9 15 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> ( 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 ) ) ) )
17 1 8 16 mpbir2and 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> F e. ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
18 ssid 
 |-  CC C_ CC
19 9 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
20 3 2 19 cncfcn 
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( A -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
21 12 18 20 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> ( A -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
22 17 21 eleqtrrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> F e. ( A -cn-> CC ) )