Theorem cnmpt21f

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt21.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
	cnmpt21f.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐿 Cn 𝑀 ) )
Assertion	cnmpt21f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		cnmpt21.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
4		cnmpt21f.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐿 Cn 𝑀 ) )
5		cntop1	⊢ ( 𝐹 ∈ ( 𝐿 Cn 𝑀 ) → 𝐿 ∈ Top )
6	4 5	syl	⊢ ( 𝜑 → 𝐿 ∈ Top )
7		toptopon2	⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
8	6 7	sylib	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
9		eqid	⊢ ∪ 𝐿 = ∪ 𝐿
10		eqid	⊢ ∪ 𝑀 = ∪ 𝑀
11	9 10	cnf	⊢ ( 𝐹 ∈ ( 𝐿 Cn 𝑀 ) → 𝐹 : ∪ 𝐿 ⟶ ∪ 𝑀 )
12	4 11	syl	⊢ ( 𝜑 → 𝐹 : ∪ 𝐿 ⟶ ∪ 𝑀 )
13	12	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ∪ 𝐿 ↦ ( 𝐹 ‘ 𝑧 ) ) )
14	13 4	eqeltrrd	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝐿 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐿 Cn 𝑀 ) )
15		fveq2	⊢ ( 𝑧 = 𝐴 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) )
16	1 2 3 8 14 15	cnmpt21	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )