Theorem cncfmpt2f

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

	Ref	Expression
Hypotheses	cncfmpt2f.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	cncfmpt2f.2	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
	cncfmpt2f.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
	cncfmpt2f.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion	cncfmpt2f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmpt2f.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		cncfmpt2f.2	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
3		cncfmpt2f.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
4		cncfmpt2f.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
5	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
6		cncfrss	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) → 𝑋 ⊆ ℂ )
7	3 6	syl	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
8		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
9	5 7 8	sylancr	⊢ ( 𝜑 → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
10		ssid	⊢ ℂ ⊆ ℂ
11		eqid	⊢ ( 𝐽 ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 )
12	5	toponrestid	⊢ 𝐽 = ( 𝐽 ↾t ℂ )
13	1 11 12	cncfcn	⊢ ( ( 𝑋 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋 –cn→ ℂ ) = ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
14	7 10 13	sylancl	⊢ ( 𝜑 → ( 𝑋 –cn→ ℂ ) = ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
15	3 14	eleqtrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
16	4 14	eleqtrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
17	9 15 16 2	cnmpt12f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
18	17 14	eleqtrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )