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 _xF
cncfmptss.2 φF:AcnB
cncfmptss.3 φCA
Assertion cncfmptss φxCFx:CcnB

Proof

Step Hyp Ref Expression
1 cncfmptss.1 _xF
2 cncfmptss.2 φF:AcnB
3 cncfmptss.3 φCA
4 3 resmptd φyAFyC=yCFy
5 cncff F:AcnBF:AB
6 2 5 syl φF:AB
7 6 feqmptd φF=yAFy
8 7 reseq1d φFC=yAFyC
9 nfcv _yF
10 nfcv _yx
11 9 10 nffv _yFx
12 nfcv _xy
13 1 12 nffv _xFy
14 fveq2 x=yFx=Fy
15 11 13 14 cbvmpt xCFx=yCFy
16 15 a1i φxCFx=yCFy
17 4 8 16 3eqtr4rd φxCFx=FC
18 rescncf CAF:AcnBFC:CcnB
19 3 2 18 sylc φFC:CcnB
20 17 19 eqeltrd φxCFx:CcnB