Theorem cnmpt1k

Description: The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cnmptk1.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmptk1.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		cnmptk1.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4		cnmpt1k.m	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑊 ) )
5		cnmpt1k.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) )
6		cnmpt1k.b	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐿 ) ) )
7		cnmpt1k.c	⊢ ( 𝑧 = 𝐴 → 𝐵 = 𝐶 )
8		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑍 )
9	1 3 5 8	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑍 )
10		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
11	10	fmpt	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑍 ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑍 )
12	9 11	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑍 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑍 )
14		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
15		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) )
16	13 14 15 7	fmptcof	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
17	16	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) )
18		topontop	⊢ ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) → 𝐿 ∈ Top )
19	3 18	syl	⊢ ( 𝜑 → 𝐿 ∈ Top )
20		topontop	⊢ ( 𝑀 ∈ ( TopOn ‘ 𝑊 ) → 𝑀 ∈ Top )
21	4 20	syl	⊢ ( 𝜑 → 𝑀 ∈ Top )
22		eqid	⊢ ( 𝑀 ↑ko 𝐿 ) = ( 𝑀 ↑ko 𝐿 )
23	22	xkotopon	⊢ ( ( 𝐿 ∈ Top ∧ 𝑀 ∈ Top ) → ( 𝑀 ↑ko 𝐿 ) ∈ ( TopOn ‘ ( 𝐿 Cn 𝑀 ) ) )
24	19 21 23	syl2anc	⊢ ( 𝜑 → ( 𝑀 ↑ko 𝐿 ) ∈ ( TopOn ‘ ( 𝐿 Cn 𝑀 ) ) )
25	21 5	xkoco1cn	⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐿 Cn 𝑀 ) ↦ ( 𝑤 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) ∈ ( ( 𝑀 ↑ko 𝐿 ) Cn ( 𝑀 ↑ko 𝐽 ) ) )
26		coeq1	⊢ ( 𝑤 = ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) → ( 𝑤 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
27	2 6 24 25 26	cnmpt11	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐽 ) ) )
28	17 27	eqeltrrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐽 ) ) )