cncfmptssg

Description: A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfmptssg.2	$⊢ F = (x \in A ⟼ E)$
	cncfmptssg.3	$⊢ φ \to F : A \underset{cn}{⟶} B$
	cncfmptssg.4	$⊢ φ \to C \subseteq A$
	cncfmptssg.5	$⊢ φ \to D \subseteq B$
	cncfmptssg.6	$⊢ (φ \land x \in C) \to E \in D$
Assertion	cncfmptssg	$⊢ φ \to (x \in C ⟼ E) : C \underset{cn}{⟶} D$

Proof

Step	Hyp	Ref	Expression
1		cncfmptssg.2	$⊢ F = (x \in A ⟼ E)$
2		cncfmptssg.3	$⊢ φ \to F : A \underset{cn}{⟶} B$
3		cncfmptssg.4	$⊢ φ \to C \subseteq A$
4		cncfmptssg.5	$⊢ φ \to D \subseteq B$
5		cncfmptssg.6	$⊢ (φ \land x \in C) \to E \in D$
6	5	fmpttd	$⊢ φ \to (x \in C ⟼ E) : C ⟶ D$
7		cncfrss2	$⊢ F : A \underset{cn}{⟶} B \to B \subseteq ℂ$
8	2 7	syl	$⊢ φ \to B \subseteq ℂ$
9	4 8	sstrd	$⊢ φ \to D \subseteq ℂ$
10	3	sselda	$⊢ (φ \land x \in C) \to x \in A$
11	1	fvmpt2	$⊢ (x \in A \land E \in D) \to F (x) = E$
12	10 5 11	syl2anc	$⊢ (φ \land x \in C) \to F (x) = E$
13	12	mpteq2dva	$⊢ φ \to (x \in C ⟼ F (x)) = (x \in C ⟼ E)$
14		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ E)$
15	1 14	nfcxfr	$⊢ \underline{Ⅎ} x F$
16	15 2 3	cncfmptss	$⊢ φ \to (x \in C ⟼ F (x)) : C \underset{cn}{⟶} B$
17	13 16	eqeltrrd	$⊢ φ \to (x \in C ⟼ E) : C \underset{cn}{⟶} B$
18		cncfcdm	$⊢ (D \subseteq ℂ \land (x \in C ⟼ E) : C \underset{cn}{⟶} B) \to ((x \in C ⟼ E) : C \underset{cn}{⟶} D \leftrightarrow (x \in C ⟼ E) : C ⟶ D)$
19	9 17 18	syl2anc	$⊢ φ \to ((x \in C ⟼ E) : C \underset{cn}{⟶} D \leftrightarrow (x \in C ⟼ E) : C ⟶ D)$
20	6 19	mpbird	$⊢ φ \to (x \in C ⟼ E) : C \underset{cn}{⟶} D$

Metamath Proof Explorer

Theorem cncfmptssg

Proof