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 A F : A D F B C = F B C

Proof

Step Hyp Ref Expression
1 ax-resscn
2 1 a1i A F : A
3 simpr A F : A F : A
4 simpl A F : A A
5 ioossre B C
6 5 a1i A F : A B C
7 eqid TopOpen fld = TopOpen fld
8 7 tgioo2 topGen ran . = TopOpen fld 𝑡
9 7 8 dvres F : A A B C D F B C = F int topGen ran . B C
10 2 3 4 6 9 syl22anc A F : A D F B C = F int topGen ran . B C
11 ioontr int topGen ran . B C = B C
12 11 reseq2i F int topGen ran . B C = F B C
13 10 12 eqtrdi A F : A D F B C = F B C