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

Metamath Proof Explorer

Theorem cnmpt12f

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 cnmptid.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt11.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
cnmpt1t.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) )
cnmpt12f.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑀 ) )
Assertion cnmpt12f ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝐽 Cn 𝑀 ) )

Proof

Step Hyp Ref Expression
1 cnmptid.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmpt11.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
3 cnmpt1t.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐽 Cn 𝐿 ) )
4 cnmpt12f.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑀 ) )
5 df-ov ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
6 5 mpteq2i ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
7 1 2 3 cnmpt1t ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐿 ) ) )
8 1 7 4 cnmpt11f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ ( 𝐽 Cn 𝑀 ) )
9 6 8 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝐽 Cn 𝑀 ) )