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 SF:AASdomFS=AF:Acn

Proof

Step Hyp Ref Expression
1 simpl2 SF:AASdomFS=AF:A
2 eqid TopOpenfld𝑡A=TopOpenfld𝑡A
3 eqid TopOpenfld=TopOpenfld
4 2 3 dvcnp2 SF:AASxdomFSFTopOpenfld𝑡ACnPTopOpenfldx
5 4 ralrimiva SF:AASxdomFSFTopOpenfld𝑡ACnPTopOpenfldx
6 raleq domFS=AxdomFSFTopOpenfld𝑡ACnPTopOpenfldxxAFTopOpenfld𝑡ACnPTopOpenfldx
7 6 biimpd domFS=AxdomFSFTopOpenfld𝑡ACnPTopOpenfldxxAFTopOpenfld𝑡ACnPTopOpenfldx
8 5 7 mpan9 SF:AASdomFS=AxAFTopOpenfld𝑡ACnPTopOpenfldx
9 3 cnfldtopon TopOpenfldTopOn
10 simpl3 SF:AASdomFS=AAS
11 simpl1 SF:AASdomFS=AS
12 10 11 sstrd SF:AASdomFS=AA
13 resttopon TopOpenfldTopOnATopOpenfld𝑡ATopOnA
14 9 12 13 sylancr SF:AASdomFS=ATopOpenfld𝑡ATopOnA
15 cncnp TopOpenfld𝑡ATopOnATopOpenfldTopOnFTopOpenfld𝑡ACnTopOpenfldF:AxAFTopOpenfld𝑡ACnPTopOpenfldx
16 14 9 15 sylancl SF:AASdomFS=AFTopOpenfld𝑡ACnTopOpenfldF:AxAFTopOpenfld𝑡ACnPTopOpenfldx
17 1 8 16 mpbir2and SF:AASdomFS=AFTopOpenfld𝑡ACnTopOpenfld
18 ssid
19 9 toponrestid TopOpenfld=TopOpenfld𝑡
20 3 2 19 cncfcn AAcn=TopOpenfld𝑡ACnTopOpenfld
21 12 18 20 sylancl SF:AASdomFS=AAcn=TopOpenfld𝑡ACnTopOpenfld
22 17 21 eleqtrrd SF:AASdomFS=AF:Acn