Theorem 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 e. A |-> E )
	cncfmptssg.3	|- ( ph -> F e. ( A -cn-> B ) )
	cncfmptssg.4	|- ( ph -> C C_ A )
	cncfmptssg.5	|- ( ph -> D C_ B )
	cncfmptssg.6	|- ( ( ph /\ x e. C ) -> E e. D )
Assertion	cncfmptssg	|- ( ph -> ( x e. C |-> E ) e. ( C -cn-> D ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmptssg.2	|- F = ( x e. A |-> E )
2		cncfmptssg.3	|- ( ph -> F e. ( A -cn-> B ) )
3		cncfmptssg.4	|- ( ph -> C C_ A )
4		cncfmptssg.5	|- ( ph -> D C_ B )
5		cncfmptssg.6	|- ( ( ph /\ x e. C ) -> E e. D )
6	5	fmpttd	|- ( ph -> ( x e. C |-> E ) : C --> D )
7		cncfrss2	|- ( F e. ( A -cn-> B ) -> B C_ CC )
8	2 7	syl	|- ( ph -> B C_ CC )
9	4 8	sstrd	|- ( ph -> D C_ CC )
10	3	sselda	|- ( ( ph /\ x e. C ) -> x e. A )
11	1	fvmpt2	|- ( ( x e. A /\ E e. D ) -> ( F ` x ) = E )
12	10 5 11	syl2anc	|- ( ( ph /\ x e. C ) -> ( F ` x ) = E )
13	12	mpteq2dva	|- ( ph -> ( x e. C |-> ( F ` x ) ) = ( x e. C |-> E ) )
14		nfmpt1	|- F/_ x ( x e. A |-> E )
15	1 14	nfcxfr	|- F/_ x F
16	15 2 3	cncfmptss	|- ( ph -> ( x e. C |-> ( F ` x ) ) e. ( C -cn-> B ) )
17	13 16	eqeltrrd	|- ( ph -> ( x e. C |-> E ) e. ( C -cn-> B ) )
18		cncfcdm	|- ( ( D C_ CC /\ ( x e. C |-> E ) e. ( C -cn-> B ) ) -> ( ( x e. C |-> E ) e. ( C -cn-> D ) <-> ( x e. C |-> E ) : C --> D ) )
19	9 17 18	syl2anc	|- ( ph -> ( ( x e. C |-> E ) e. ( C -cn-> D ) <-> ( x e. C |-> E ) : C --> D ) )
20	6 19	mpbird	|- ( ph -> ( x e. C |-> E ) e. ( C -cn-> D ) )