Theorem cnmptk1

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

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

Proof

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