Theorem cncfmpt2f

Description: Composition of continuous functions. -cn-> analogue of cnmpt12f . (Contributed by Mario Carneiro, 3-Sep-2014)

	Ref	Expression
Hypotheses	cncfmpt2f.1	|- J = ( TopOpen ` CCfld )
	cncfmpt2f.2	|- ( ph -> F e. ( ( J tX J ) Cn J ) )
	cncfmpt2f.3	|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
	cncfmpt2f.4	|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
Assertion	cncfmpt2f	|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmpt2f.1	|- J = ( TopOpen ` CCfld )
2		cncfmpt2f.2	|- ( ph -> F e. ( ( J tX J ) Cn J ) )
3		cncfmpt2f.3	|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
4		cncfmpt2f.4	|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
5	1	cnfldtopon	|- J e. ( TopOn ` CC )
6		cncfrss	|- ( ( x e. X |-> A ) e. ( X -cn-> CC ) -> X C_ CC )
7	3 6	syl	|- ( ph -> X C_ CC )
8		resttopon	|- ( ( J e. ( TopOn ` CC ) /\ X C_ CC ) -> ( J |`t X ) e. ( TopOn ` X ) )
9	5 7 8	sylancr	|- ( ph -> ( J |`t X ) e. ( TopOn ` X ) )
10		ssid	|- CC C_ CC
11		eqid	|- ( J |`t X ) = ( J |`t X )
12	5	toponrestid	|- J = ( J |`t CC )
13	1 11 12	cncfcn	|- ( ( X C_ CC /\ CC C_ CC ) -> ( X -cn-> CC ) = ( ( J |`t X ) Cn J ) )
14	7 10 13	sylancl	|- ( ph -> ( X -cn-> CC ) = ( ( J |`t X ) Cn J ) )
15	3 14	eleqtrd	|- ( ph -> ( x e. X |-> A ) e. ( ( J |`t X ) Cn J ) )
16	4 14	eleqtrd	|- ( ph -> ( x e. X |-> B ) e. ( ( J |`t X ) Cn J ) )
17	9 15 16 2	cnmpt12f	|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( ( J |`t X ) Cn J ) )
18	17 14	eleqtrrd	|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) )