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