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	$⊢ \underline{Ⅎ} x F$
	cncfmptss.2	$⊢ φ \to F : A \underset{cn}{⟶} B$
	cncfmptss.3	$⊢ φ \to C \subseteq A$
Assertion	cncfmptss	$⊢ φ \to (x \in C ⟼ F (x)) : C \underset{cn}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		cncfmptss.1	$⊢ \underline{Ⅎ} x F$
2		cncfmptss.2	$⊢ φ \to F : A \underset{cn}{⟶} B$
3		cncfmptss.3	$⊢ φ \to C \subseteq A$
4	3	resmptd	$⊢ φ \to {(y \in A ⟼ F (y)) ↾}_{C} = (y \in C ⟼ F (y))$
5		cncff	$⊢ F : A \underset{cn}{⟶} B \to F : A ⟶ B$
6	2 5	syl	$⊢ φ \to F : A ⟶ B$
7	6	feqmptd	$⊢ φ \to F = (y \in A ⟼ F (y))$
8	7	reseq1d	$⊢ φ \to {F ↾}_{C} = {(y \in A ⟼ F (y)) ↾}_{C}$
9		nfcv	$⊢ \underline{Ⅎ} y F$
10		nfcv	$⊢ \underline{Ⅎ} y x$
11	9 10	nffv	$⊢ \underline{Ⅎ} y F (x)$
12		nfcv	$⊢ \underline{Ⅎ} x y$
13	1 12	nffv	$⊢ \underline{Ⅎ} x F (y)$
14		fveq2	$⊢ x = y \to F (x) = F (y)$
15	11 13 14	cbvmpt	$⊢ (x \in C ⟼ F (x)) = (y \in C ⟼ F (y))$
16	15	a1i	$⊢ φ \to (x \in C ⟼ F (x)) = (y \in C ⟼ F (y))$
17	4 8 16	3eqtr4rd	$⊢ φ \to (x \in C ⟼ F (x)) = {F ↾}_{C}$
18		rescncf	$⊢ C \subseteq A \to (F : A \underset{cn}{⟶} B \to ({F ↾}_{C}) : C \underset{cn}{⟶} B)$
19	3 2 18	sylc	$⊢ φ \to ({F ↾}_{C}) : C \underset{cn}{⟶} B$
20	17 19	eqeltrd	$⊢ φ \to (x \in C ⟼ F (x)) : C \underset{cn}{⟶} B$

Metamath Proof Explorer

Theorem cncfmptss

Proof