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