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