Theorem cnmpt22f

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 𝐿 ) )
	cnmpt2t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
	cnmpt22f.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
Assertion	cnmpt22f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		cnmpt21.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
4		cnmpt2t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
5		cnmpt22f.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
6		cntop2	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) → 𝐿 ∈ Top )
7	3 6	syl	⊢ ( 𝜑 → 𝐿 ∈ Top )
8		toptopon2	⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
9	7 8	sylib	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
10		cntop2	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) → 𝑀 ∈ Top )
11	4 10	syl	⊢ ( 𝜑 → 𝑀 ∈ Top )
12		toptopon2	⊢ ( 𝑀 ∈ Top ↔ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
13	11 12	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
14		txtopon	⊢ ( ( 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) ) → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( ∪ 𝐿 × ∪ 𝑀 ) ) )
15	9 13 14	syl2anc	⊢ ( 𝜑 → ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( ∪ 𝐿 × ∪ 𝑀 ) ) )
16		cntop2	⊢ ( 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) → 𝑁 ∈ Top )
17	5 16	syl	⊢ ( 𝜑 → 𝑁 ∈ Top )
18		toptopon2	⊢ ( 𝑁 ∈ Top ↔ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
19	17 18	sylib	⊢ ( 𝜑 → 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
20		cnf2	⊢ ( ( ( 𝐿 ×t 𝑀 ) ∈ ( TopOn ‘ ( ∪ 𝐿 × ∪ 𝑀 ) ) ∧ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) ∧ 𝐹 ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) ) → 𝐹 : ( ∪ 𝐿 × ∪ 𝑀 ) ⟶ ∪ 𝑁 )
21	15 19 5 20	syl3anc	⊢ ( 𝜑 → 𝐹 : ( ∪ 𝐿 × ∪ 𝑀 ) ⟶ ∪ 𝑁 )
22	21	ffnd	⊢ ( 𝜑 → 𝐹 Fn ( ∪ 𝐿 × ∪ 𝑀 ) )
23		fnov	⊢ ( 𝐹 Fn ( ∪ 𝐿 × ∪ 𝑀 ) ↔ 𝐹 = ( 𝑧 ∈ ∪ 𝐿 , 𝑤 ∈ ∪ 𝑀 ↦ ( 𝑧 𝐹 𝑤 ) ) )
24	22 23	sylib	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ∪ 𝐿 , 𝑤 ∈ ∪ 𝑀 ↦ ( 𝑧 𝐹 𝑤 ) ) )
25	24 5	eqeltrrd	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝐿 , 𝑤 ∈ ∪ 𝑀 ↦ ( 𝑧 𝐹 𝑤 ) ) ∈ ( ( 𝐿 ×t 𝑀 ) Cn 𝑁 ) )
26		oveq12	⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → ( 𝑧 𝐹 𝑤 ) = ( 𝐴 𝐹 𝐵 ) )
27	1 2 3 4 9 13 25 26	cnmpt22	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )