Metamath Proof Explorer


Theorem dvresioo

Description: Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dvresioo AF:ADFBC=FBC

Proof

Step Hyp Ref Expression
1 ax-resscn
2 1 a1i AF:A
3 simpr AF:AF:A
4 simpl AF:AA
5 ioossre BC
6 5 a1i AF:ABC
7 eqid TopOpenfld=TopOpenfld
8 7 tgioo2 topGenran.=TopOpenfld𝑡
9 7 8 dvres F:AABCDFBC=FinttopGenran.BC
10 2 3 4 6 9 syl22anc AF:ADFBC=FinttopGenran.BC
11 ioontr inttopGenran.BC=BC
12 11 reseq2i FinttopGenran.BC=FBC
13 10 12 eqtrdi AF:ADFBC=FBC