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

Metamath Proof Explorer

Theorem cnmpt11f

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 𝐾 ) )
		cnmpt11f.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐾 Cn 𝐿 ) )
	Assertion	cnmpt11f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt11.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) )
3		cnmpt11f.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐾 Cn 𝐿 ) )
4		cntop2	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
5	2 4	syl	⊢ ( 𝜑 → 𝐾 ∈ Top )
6		toptopon2	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
7	5 6	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
8		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
9		eqid	⊢ ∪ 𝐿 = ∪ 𝐿
10	8 9	cnf	⊢ ( 𝐹 ∈ ( 𝐾 Cn 𝐿 ) → 𝐹 : ∪ 𝐾 ⟶ ∪ 𝐿 )
11	3 10	syl	⊢ ( 𝜑 → 𝐹 : ∪ 𝐾 ⟶ ∪ 𝐿 )
12	11	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ∪ 𝐾 ↦ ( 𝐹 ‘ 𝑦 ) ) )
13	12 3	eqeltrrd	⊢ ( 𝜑 → ( 𝑦 ∈ ∪ 𝐾 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ ( 𝐾 Cn 𝐿 ) )
14		fveq2	⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
15	1 2 7 13 14	cnmpt11	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐿 ) )