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