Theorem cnmptk2 23743

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

Hypotheses

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

Assertion

Ref	Expression
cnmptk2	⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))

Distinct variable groups:   𝑥,𝐽   𝑥,𝐾   𝑥,𝐿   𝑥,𝑦,𝑋   𝑥,𝑌,𝑦   𝜑,𝑥,𝑦   𝑦,𝑍

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐽(𝑦)   𝐾(𝑦)   𝐿(𝑦)   𝑍(𝑥)

Proof of Theorem cnmptk2

Dummy variables 𝑓 𝑘 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nffvmpt1 6878	. . . . 5 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)
2		nfcv 2924	. . . . 5 ⊢ Ⅎ𝑥𝑘
3	1, 2	nffv 6877	. . . 4 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)
4		nfcv 2924	. . . . . . 7 ⊢ Ⅎ𝑦𝑋
5		nfmpt1 5199	. . . . . . 7 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ 𝐴)
6	4, 5	nfmpt 5198	. . . . . 6 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))
7		nfcv 2924	. . . . . 6 ⊢ Ⅎ𝑦𝑤
8	6, 7	nffv 6877	. . . . 5 ⊢ Ⅎ𝑦((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)
9		nfcv 2924	. . . . 5 ⊢ Ⅎ𝑦𝑘
10	8, 9	nffv 6877	. . . 4 ⊢ Ⅎ𝑦(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)
11		nfcv 2924	. . . 4 ⊢ Ⅎ𝑤(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦)
12		nfcv 2924	. . . 4 ⊢ Ⅎ𝑘(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦)
13		fveq2 6867	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥))
14	13	fveq1d 6869	. . . . 5 ⊢ (𝑤 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑘))
15		fveq2 6867	. . . . 5 ⊢ (𝑘 = 𝑦 → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑘) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦))
16	14, 15	sylan9eq 2817	. . . 4 ⊢ ((𝑤 = 𝑥 ∧ 𝑘 = 𝑦) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦))
17	3, 10, 11, 12, 16	cbvmpo 7490	. . 3 ⊢ (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦))
18		simplr 778	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑥 ∈ 𝑋)
19		cnmptk1p.j	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
20		cnmptk1p.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp)
21		nllytop 23530	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
22	20, 21	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Top)
23		cnmptk1p.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))
24		topontop 22970	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top)
25	23, 24	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ Top)
26		eqid 2762	. . . . . . . . . . . . 13 ⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾)
27	26	xkotopon 23657	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
28	22, 25, 27	syl2anc 593	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
29		cnmptk2.a	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
30		cnf2 23306	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿))
31	19, 28, 29, 30	syl3anc 1390	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿))
32	31	fvmptelcdm 7094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿))
33	32	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿))
34		eqid 2762	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))
35	34	fvmpt2 6987	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥) = (𝑦 ∈ 𝑌 ↦ 𝐴))
36	18, 33, 35	syl2anc 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥) = (𝑦 ∈ 𝑌 ↦ 𝐴))
37	36	fveq1d 6869	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑦))
38		simpr 488	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
39		cnmptk1p.k	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
40	39	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌))
41	23	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘𝑍))
42		cnf2 23306	. . . . . . . . 9 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍)
43	40, 41, 32, 42	syl3anc 1390	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍)
44	43	fvmptelcdm 7094	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑍)
45		eqid 2762	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴)
46	45	fvmpt2 6987	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑌 ∧ 𝐴 ∈ 𝑍) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑦) = 𝐴)
47	38, 44, 46	syl2anc 593	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑦) = 𝐴)
48	37, 47	eqtrd 2797	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) = 𝐴)
49	48	3impa 1122	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) = 𝐴)
50	49	mpoeq3dva 7473	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))
51	17, 50	eqtrid 2809	. 2 ⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))
52	19, 39	cnmpt1st 23725	. . . 4 ⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ 𝑤) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
53	19, 39, 52, 29	cnmpt21f 23729	. . 3 ⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ↑ko 𝐾)))
54	19, 39	cnmpt2nd 23726	. . 3 ⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ 𝑘) ∈ ((𝐽 ×t 𝐾) Cn 𝐾))
55		eqid 2762	. . . . 5 ⊢ (𝐾 Cn 𝐿) = (𝐾 Cn 𝐿)
56		toponuni 22971	. . . . . 6 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
57	39, 56	syl 17	. . . . 5 ⊢ (𝜑 → 𝑌 = ∪ 𝐾)
58		mpoeq12 7469	. . . . 5 ⊢ (((𝐾 Cn 𝐿) = (𝐾 Cn 𝐿) ∧ 𝑌 = ∪ 𝐾) → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)))
59	55, 57, 58	sylancr 596	. . . 4 ⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)))
60		eqid 2762	. . . . . 6 ⊢ ∪ 𝐾 = ∪ 𝐾
61		eqid 2762	. . . . . 6 ⊢ (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧))
62	60, 61	xkofvcn 23741	. . . . 5 ⊢ ((𝐾 ∈ 𝑛-Locally Comp ∧ 𝐿 ∈ Top) → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ↑ko 𝐾) ×t 𝐾) Cn 𝐿))
63	20, 25, 62	syl2anc 593	. . . 4 ⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ↑ko 𝐾) ×t 𝐾) Cn 𝐿))
64	59, 63	eqeltrd 2862	. . 3 ⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ↑ko 𝐾) ×t 𝐾) Cn 𝐿))
65		fveq1 6866	. . . 4 ⊢ (𝑓 = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) → (𝑓‘𝑧) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑧))
66		fveq2 6867	. . . 4 ⊢ (𝑧 = 𝑘 → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑧) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘))
67	65, 66	sylan9eq 2817	. . 3 ⊢ ((𝑓 = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) ∧ 𝑧 = 𝑘) → (𝑓‘𝑧) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘))
68	19, 39, 53, 54, 28, 39, 64, 67	cnmpt22 23731	. 2 ⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
69	51, 68	eqeltrrd 2863	1 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∪ cuni 4865   ↦ cmpt 5181  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396   ∈ cmpo 7398  Topctop 22950  TopOnctopon 22967   Cn ccn 23281  Compccmp 23443  𝑛-Locally cnlly 23522   ×_t ctx 23617   ↑_ko cxko 23618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-1o 8437  df-2o 8438  df-map 8810  df-ixp 8880  df-en 8928  df-dom 8929  df-fin 8931  df-fi 9357  df-rest 17451  df-topgen 17472  df-pt 17473  df-top 22951  df-topon 22968  df-bases 23003  df-ntr 23077  df-nei 23155  df-cn 23284  df-cnp 23285  df-cmp 23444  df-nlly 23524  df-tx 23619  df-xko 23620

This theorem is referenced by:  xkocnv  23871