Theorem cncfcompt2

Description: Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	cncfcompt2.xph	⊢ Ⅎ 𝑥 𝜑
	cncfcompt2.ab	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐵 ) )
	cncfcompt2.cd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∈ ( 𝐶 –cn→ 𝐸 ) )
	cncfcompt2.bc	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
	cncfcompt2.st	⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
Assertion	cncfcompt2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ∈ ( 𝐴 –cn→ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfcompt2.xph	⊢ Ⅎ 𝑥 𝜑
2		cncfcompt2.ab	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐵 ) )
3		cncfcompt2.cd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∈ ( 𝐶 –cn→ 𝐸 ) )
4		cncfcompt2.bc	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
5		cncfcompt2.st	⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
6	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
7		cncff	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ 𝐵 )
8	2 7	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ 𝐵 )
9	8	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝐵 )
10	6 9	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝐶 )
11	10	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑅 ∈ 𝐶 ) )
12	1 11	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐶 )
13		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
14		eqidd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) = ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) )
15	12 13 14 5	fmptcof	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
16	15	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) = ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) )
17		cncfrss	⊢ ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∈ ( 𝐶 –cn→ 𝐸 ) → 𝐶 ⊆ ℂ )
18	3 17	syl	⊢ ( 𝜑 → 𝐶 ⊆ ℂ )
19		cncfss	⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) ⊆ ( 𝐴 –cn→ 𝐶 ) )
20	4 18 19	syl2anc	⊢ ( 𝜑 → ( 𝐴 –cn→ 𝐵 ) ⊆ ( 𝐴 –cn→ 𝐶 ) )
21	20 2	sseldd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐶 ) )
22	21 3	cncfco	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) ∈ ( 𝐴 –cn→ 𝐸 ) )
23	16 22	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ∈ ( 𝐴 –cn→ 𝐸 ) )