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 | |
|
cncfmptss.2 | |
||
cncfmptss.3 | |
||
Assertion | cncfmptss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cncfmptss.1 | |
|
2 | cncfmptss.2 | |
|
3 | cncfmptss.3 | |
|
4 | 3 | resmptd | |
5 | cncff | |
|
6 | 2 5 | syl | |
7 | 6 | feqmptd | |
8 | 7 | reseq1d | |
9 | nfcv | |
|
10 | nfcv | |
|
11 | 9 10 | nffv | |
12 | nfcv | |
|
13 | 1 12 | nffv | |
14 | fveq2 | |
|
15 | 11 13 14 | cbvmpt | |
16 | 15 | a1i | |
17 | 4 8 16 | 3eqtr4rd | |
18 | rescncf | |
|
19 | 3 2 18 | sylc | |
20 | 17 19 | eqeltrd | |