Theorem cnmptkp

Description: The evaluation of the inner function in 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 ‘ 𝑍 ) )
	cnmptkp.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
	cnmptkp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
	cnmptkp.c	⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐶 )
Assertion	cnmptkp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ∈ ( 𝐽 Cn 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptk1.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmptk1.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		cnmptk1.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4		cnmptkp.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
5		cnmptkp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
6		cnmptkp.c	⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐶 )
7		eqid	⊢ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 )
8	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑌 )
9	6	eleq1d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿 ) )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
11		topontop	⊢ ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) → 𝐿 ∈ Top )
12	3 11	syl	⊢ ( 𝜑 → 𝐿 ∈ Top )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐿 ∈ Top )
14		toptopon2	⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
15	13 14	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
16		topontop	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
17	2 16	syl	⊢ ( 𝜑 → 𝐾 ∈ Top )
18		eqid	⊢ ( 𝐿 ↑ko 𝐾 ) = ( 𝐿 ↑ko 𝐾 )
19	18	xkotopon	⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
20	17 12 19	syl2anc	⊢ ( 𝜑 → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
21		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
22	1 20 4 21	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
23	22	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) )
24		cnf2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ ∪ 𝐿 )
25	10 15 23 24	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ ∪ 𝐿 )
26	7	fmpt	⊢ ( ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 ↔ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ ∪ 𝐿 )
27	25 26	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 )
28	9 27 8	rspcdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ∪ 𝐿 )
29	7 6 8 28	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) = 𝐶 )
30	29	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
31		toponuni	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
32	2 31	syl	⊢ ( 𝜑 → 𝑌 = ∪ 𝐾 )
33	5 32	eleqtrd	⊢ ( 𝜑 → 𝐵 ∈ ∪ 𝐾 )
34		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
35	34	xkopjcn	⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝐵 ∈ ∪ 𝐾 ) → ( 𝑤 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑤 ‘ 𝐵 ) ) ∈ ( ( 𝐿 ↑ko 𝐾 ) Cn 𝐿 ) )
36	17 12 33 35	syl3anc	⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑤 ‘ 𝐵 ) ) ∈ ( ( 𝐿 ↑ko 𝐾 ) Cn 𝐿 ) )
37		fveq1	⊢ ( 𝑤 = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) → ( 𝑤 ‘ 𝐵 ) = ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) )
38	1 4 20 36 37	cnmpt11	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
39	30 38	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ∈ ( 𝐽 Cn 𝐿 ) )