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

Metamath Proof Explorer

Theorem cncfcompt2

Description: Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses cncfcompt2.xph 
|- F/ x ph
cncfcompt2.ab 
|- ( ph -> ( x e. A |-> R ) e. ( A -cn-> B ) )
cncfcompt2.cd 
|- ( ph -> ( y e. C |-> S ) e. ( C -cn-> E ) )
cncfcompt2.bc 
|- ( ph -> B C_ C )
cncfcompt2.st 
|- ( y = R -> S = T )
Assertion cncfcompt2 
|- ( ph -> ( x e. A |-> T ) e. ( A -cn-> E ) )

Proof

Step Hyp Ref Expression
1 cncfcompt2.xph 
 |-  F/ x ph
2 cncfcompt2.ab 
 |-  ( ph -> ( x e. A |-> R ) e. ( A -cn-> B ) )
3 cncfcompt2.cd 
 |-  ( ph -> ( y e. C |-> S ) e. ( C -cn-> E ) )
4 cncfcompt2.bc 
 |-  ( ph -> B C_ C )
5 cncfcompt2.st 
 |-  ( y = R -> S = T )
6 4 adantr 
 |-  ( ( ph /\ x e. A ) -> B C_ C )
7 cncff 
 |-  ( ( x e. A |-> R ) e. ( A -cn-> B ) -> ( x e. A |-> R ) : A --> B )
8 2 7 syl 
 |-  ( ph -> ( x e. A |-> R ) : A --> B )
9 8 fvmptelcdm 
 |-  ( ( ph /\ x e. A ) -> R e. B )
10 6 9 sseldd 
 |-  ( ( ph /\ x e. A ) -> R e. C )
11 10 ex 
 |-  ( ph -> ( x e. A -> R e. C ) )
12 1 11 ralrimi 
 |-  ( ph -> A. x e. A R e. C )
13 eqidd 
 |-  ( ph -> ( x e. A |-> R ) = ( x e. A |-> R ) )
14 eqidd 
 |-  ( ph -> ( y e. C |-> S ) = ( y e. C |-> S ) )
15 12 13 14 5 fmptcof 
 |-  ( ph -> ( ( y e. C |-> S ) o. ( x e. A |-> R ) ) = ( x e. A |-> T ) )
16 15 eqcomd 
 |-  ( ph -> ( x e. A |-> T ) = ( ( y e. C |-> S ) o. ( x e. A |-> R ) ) )
17 cncfrss 
 |-  ( ( y e. C |-> S ) e. ( C -cn-> E ) -> C C_ CC )
18 3 17 syl 
 |-  ( ph -> C C_ CC )
19 cncfss 
 |-  ( ( B C_ C /\ C C_ CC ) -> ( A -cn-> B ) C_ ( A -cn-> C ) )
20 4 18 19 syl2anc 
 |-  ( ph -> ( A -cn-> B ) C_ ( A -cn-> C ) )
21 20 2 sseldd 
 |-  ( ph -> ( x e. A |-> R ) e. ( A -cn-> C ) )
22 21 3 cncfco 
 |-  ( ph -> ( ( y e. C |-> S ) o. ( x e. A |-> R ) ) e. ( A -cn-> E ) )
23 16 22 eqeltrd 
 |-  ( ph -> ( x e. A |-> T ) e. ( A -cn-> E ) )