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

Metamath Proof Explorer

Theorem cncfcompt

Description: Composition of continuous functions. A generalization of cncfmpt1f to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfcompt.bcn 
|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> C ) )
cncfcompt.f 
|- ( ph -> F e. ( C -cn-> D ) )
Assertion cncfcompt 
|- ( ph -> ( x e. A |-> ( F ` B ) ) e. ( A -cn-> D ) )

Proof

Step Hyp Ref Expression
1 cncfcompt.bcn 
 |-  ( ph -> ( x e. A |-> B ) e. ( A -cn-> C ) )
2 cncfcompt.f 
 |-  ( ph -> F e. ( C -cn-> D ) )
3 cncff 
 |-  ( F e. ( C -cn-> D ) -> F : C --> D )
4 2 3 syl 
 |-  ( ph -> F : C --> D )
5 4 adantr 
 |-  ( ( ph /\ x e. A ) -> F : C --> D )
6 cncff 
 |-  ( ( x e. A |-> B ) e. ( A -cn-> C ) -> ( x e. A |-> B ) : A --> C )
7 1 6 syl 
 |-  ( ph -> ( x e. A |-> B ) : A --> C )
8 7 fvmptelcdm 
 |-  ( ( ph /\ x e. A ) -> B e. C )
9 5 8 ffvelcdmd 
 |-  ( ( ph /\ x e. A ) -> ( F ` B ) e. D )
10 9 fmpttd 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) : A --> D )
11 cncfrss2 
 |-  ( F e. ( C -cn-> D ) -> D C_ CC )
12 2 11 syl 
 |-  ( ph -> D C_ CC )
13 eqidd 
 |-  ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
14 4 feqmptd 
 |-  ( ph -> F = ( y e. C |-> ( F ` y ) ) )
15 fveq2 
 |-  ( y = B -> ( F ` y ) = ( F ` B ) )
16 8 13 14 15 fmptco 
 |-  ( ph -> ( F o. ( x e. A |-> B ) ) = ( x e. A |-> ( F ` B ) ) )
17 ssid 
 |-  CC C_ CC
18 cncfss 
 |-  ( ( D C_ CC /\ CC C_ CC ) -> ( C -cn-> D ) C_ ( C -cn-> CC ) )
19 12 17 18 sylancl 
 |-  ( ph -> ( C -cn-> D ) C_ ( C -cn-> CC ) )
20 19 2 sseldd 
 |-  ( ph -> F e. ( C -cn-> CC ) )
21 1 20 cncfco 
 |-  ( ph -> ( F o. ( x e. A |-> B ) ) e. ( A -cn-> CC ) )
22 16 21 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) e. ( A -cn-> CC ) )
23 cncfcdm 
 |-  ( ( D C_ CC /\ ( x e. A |-> ( F ` B ) ) e. ( A -cn-> CC ) ) -> ( ( x e. A |-> ( F ` B ) ) e. ( A -cn-> D ) <-> ( x e. A |-> ( F ` B ) ) : A --> D ) )
24 12 22 23 syl2anc 
 |-  ( ph -> ( ( x e. A |-> ( F ` B ) ) e. ( A -cn-> D ) <-> ( x e. A |-> ( F ` B ) ) : A --> D ) )
25 10 24 mpbird 
 |-  ( ph -> ( x e. A |-> ( F ` B ) ) e. ( A -cn-> D ) )