This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reldv

Description: The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion reldv 
|- Rel ( S _D F )

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) )
2 1 rgenw 
 |-  A. x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) Rel ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) )
3 reliun 
 |-  ( Rel U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) <-> A. x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) Rel ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) )
4 2 3 mpbir 
 |-  Rel U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) )
5 df-rel 
 |-  ( Rel U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) <-> U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( _V X. _V ) )
6 4 5 mpbi 
 |-  U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( _V X. _V )
7 6 rgenw 
 |-  A. f e. ( CC ^pm s ) U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( _V X. _V )
8 7 rgenw 
 |-  A. s e. ~P CC A. f e. ( CC ^pm s ) U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( _V X. _V )
9 df-dv 
 |-  _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) )
10 9 ovmptss 
 |-  ( A. s e. ~P CC A. f e. ( CC ^pm s ) U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) C_ ( _V X. _V ) -> ( S _D F ) C_ ( _V X. _V ) )
11 8 10 ax-mp 
 |-  ( S _D F ) C_ ( _V X. _V )
12 df-rel 
 |-  ( Rel ( S _D F ) <-> ( S _D F ) C_ ( _V X. _V ) )
13 11 12 mpbir 
 |-  Rel ( S _D F )