Theorem cnmptkk

Description: The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmptkk.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmptkk.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	cnmptkk.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
	cnmptkk.m	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑊 ) )
	cnmptkk.n	⊢ ( 𝜑 → 𝐿 ∈ 𝑛-Locally Comp )
	cnmptkk.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
	cnmptkk.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ( 𝐽 Cn ( 𝑀 ↑ko 𝐿 ) ) )
	cnmptkk.c	⊢ ( 𝑧 = 𝐴 → 𝐵 = 𝐶 )
Assertion	cnmptkk	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∈ ( 𝐽 Cn ( 𝑀 ↑ko 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptkk.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmptkk.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		cnmptkk.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4		cnmptkk.m	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑊 ) )
5		cnmptkk.n	⊢ ( 𝜑 → 𝐿 ∈ 𝑛-Locally Comp )
6		cnmptkk.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
7		cnmptkk.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ( 𝐽 Cn ( 𝑀 ↑ko 𝐿 ) ) )
8		cnmptkk.c	⊢ ( 𝑧 = 𝐴 → 𝐵 = 𝐶 )
9	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
11		topontop	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
12	2 11	syl	⊢ ( 𝜑 → 𝐾 ∈ Top )
13		nllytop	⊢ ( 𝐿 ∈ 𝑛-Locally Comp → 𝐿 ∈ Top )
14	5 13	syl	⊢ ( 𝜑 → 𝐿 ∈ Top )
15		eqid	⊢ ( 𝐿 ↑ko 𝐾 ) = ( 𝐿 ↑ko 𝐾 )
16	15	xkotopon	⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
17	12 14 16	syl2anc	⊢ ( 𝜑 → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
18		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
19	1 17 6 18	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
20	19	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) )
21		cnf2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ 𝑍 )
22	9 10 20 21	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ 𝑍 )
23		eqid	⊢ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 )
24	23	fmpt	⊢ ( ∀ 𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 ↔ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ 𝑍 )
25	22 24	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 )
26		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
27		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) )
28	25 26 27 8	fmptcof	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
29	28	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )
30		topontop	⊢ ( 𝑀 ∈ ( TopOn ‘ 𝑊 ) → 𝑀 ∈ Top )
31	4 30	syl	⊢ ( 𝜑 → 𝑀 ∈ Top )
32		eqid	⊢ ( 𝑀 ↑ko 𝐿 ) = ( 𝑀 ↑ko 𝐿 )
33	32	xkotopon	⊢ ( ( 𝐿 ∈ Top ∧ 𝑀 ∈ Top ) → ( 𝑀 ↑ko 𝐿 ) ∈ ( TopOn ‘ ( 𝐿 Cn 𝑀 ) ) )
34	14 31 33	syl2anc	⊢ ( 𝜑 → ( 𝑀 ↑ko 𝐿 ) ∈ ( TopOn ‘ ( 𝐿 Cn 𝑀 ) ) )
35		eqid	⊢ ( 𝑓 ∈ ( 𝐿 Cn 𝑀 ) , 𝑔 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ ( 𝐿 Cn 𝑀 ) , 𝑔 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑓 ∘ 𝑔 ) )
36	35	xkococn	⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ 𝑛-Locally Comp ∧ 𝑀 ∈ Top ) → ( 𝑓 ∈ ( 𝐿 Cn 𝑀 ) , 𝑔 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ ( ( ( 𝑀 ↑ko 𝐿 ) ×t ( 𝐿 ↑ko 𝐾 ) ) Cn ( 𝑀 ↑ko 𝐾 ) ) )
37	12 5 31 36	syl3anc	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐿 Cn 𝑀 ) , 𝑔 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ ( ( ( 𝑀 ↑ko 𝐿 ) ×t ( 𝐿 ↑ko 𝐾 ) ) Cn ( 𝑀 ↑ko 𝐾 ) ) )
38		coeq1	⊢ ( 𝑓 = ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) → ( 𝑓 ∘ 𝑔 ) = ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ 𝑔 ) )
39		coeq2	⊢ ( 𝑔 = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) → ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ 𝑔 ) = ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) )
40	38 39	sylan9eq	⊢ ( ( 𝑓 = ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∧ 𝑔 = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) → ( 𝑓 ∘ 𝑔 ) = ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) )
41	1 7 6 34 17 37 40	cnmpt12	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ) ∈ ( 𝐽 Cn ( 𝑀 ↑ko 𝐾 ) ) )
42	29 41	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) ∈ ( 𝐽 Cn ( 𝑀 ↑ko 𝐾 ) ) )