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	fvmptelrn	|- ( ( ph /\ x e. A ) -> B e. C )
9	5 8	ffvelrnd	|- ( ( 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		cncffvrn	|- ( ( 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 ) )