Metamath Proof Explorer

Theorem cncfmptss

Description: A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses cncfmptss.1 
|- F/_ x F
cncfmptss.2 
|- ( ph -> F e. ( A -cn-> B ) )
cncfmptss.3 
|- ( ph -> C C_ A )
Assertion cncfmptss 
|- ( ph -> ( x e. C |-> ( F ` x ) ) e. ( C -cn-> B ) )

Proof

Step Hyp Ref Expression
1 cncfmptss.1 
 |-  F/_ x F
2 cncfmptss.2 
 |-  ( ph -> F e. ( A -cn-> B ) )
3 cncfmptss.3 
 |-  ( ph -> C C_ A )
4 3 resmptd 
 |-  ( ph -> ( ( y e. A |-> ( F ` y ) ) |` C ) = ( y e. C |-> ( F ` y ) ) )
5 cncff 
 |-  ( F e. ( A -cn-> B ) -> F : A --> B )
6 2 5 syl 
 |-  ( ph -> F : A --> B )
7 6 feqmptd 
 |-  ( ph -> F = ( y e. A |-> ( F ` y ) ) )
8 7 reseq1d 
 |-  ( ph -> ( F |` C ) = ( ( y e. A |-> ( F ` y ) ) |` C ) )
9 nfcv 
 |-  F/_ y F
10 nfcv 
 |-  F/_ y x
11 9 10 nffv 
 |-  F/_ y ( F ` x )
12 nfcv 
 |-  F/_ x y
13 1 12 nffv 
 |-  F/_ x ( F ` y )
14 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
15 11 13 14 cbvmpt 
 |-  ( x e. C |-> ( F ` x ) ) = ( y e. C |-> ( F ` y ) )
16 15 a1i 
 |-  ( ph -> ( x e. C |-> ( F ` x ) ) = ( y e. C |-> ( F ` y ) ) )
17 4 8 16 3eqtr4rd 
 |-  ( ph -> ( x e. C |-> ( F ` x ) ) = ( F |` C ) )
18 rescncf 
 |-  ( C C_ A -> ( F e. ( A -cn-> B ) -> ( F |` C ) e. ( C -cn-> B ) ) )
19 3 2 18 sylc 
 |-  ( ph -> ( F |` C ) e. ( C -cn-> B ) )
20 17 19 eqeltrd 
 |-  ( ph -> ( x e. C |-> ( F ` x ) ) e. ( C -cn-> B ) )