Metamath Proof Explorer


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 𝑀 ) )