This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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