Theorem cnmptk1p

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

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

Proof

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