This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )