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	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) )
	cncfcompt.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) )
Assertion	cncfcompt	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfcompt.bcn	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) )
2		cncfcompt.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) )
3		cncff	⊢ ( 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) → 𝐹 : 𝐶 ⟶ 𝐷 )
4	2 3	syl	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐷 )
5	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐶 ⟶ 𝐷 )
6		cncff	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
7	1 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
8	7	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
9	5 8	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 )
10	9	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ 𝐷 )
11		cncfrss2	⊢ ( 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) → 𝐷 ⊆ ℂ )
12	2 11	syl	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
13		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
14	4	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) ) )
15		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
16	8 13 14 15	fmptco	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) )
17		ssid	⊢ ℂ ⊆ ℂ
18		cncfss	⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐶 –cn→ 𝐷 ) ⊆ ( 𝐶 –cn→ ℂ ) )
19	12 17 18	sylancl	⊢ ( 𝜑 → ( 𝐶 –cn→ 𝐷 ) ⊆ ( 𝐶 –cn→ ℂ ) )
20	19 2	sseldd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ ℂ ) )
21	1 20	cncfco	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
22	16 21	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
23		cncffvrn	⊢ ( ( 𝐷 ⊆ ℂ ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ 𝐷 ) )
24	12 22 23	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ 𝐷 ) )
25	10 24	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) )