Metamath Proof Explorer

Theorem dvfg

Description: Explicitly write out the functionality condition on derivative for S = RR and CC . (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Assertion dvfg 
|- ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 recnperf 
 |-  ( S e. { RR , CC } -> ( ( TopOpen ` CCfld ) |`t S ) e. Perf )
3 1 perfdvf 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) e. Perf -> ( S _D F ) : dom ( S _D F ) --> CC )
4 2 3 syl 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )