Metamath Proof Explorer

Theorem cnmptk2

Description: The uncurrying of a curried function is 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 )
cnmptk2.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
Assertion cnmptk2 ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnmptk1p.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmptk1p.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmptk1p.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4 cnmptk1p.n ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Comp )
5 cnmptk2.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
6 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 )
7 nfcv ⊢ Ⅎ 𝑥 𝑘
8 6 7 nffv ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 )
9 nfcv ⊢ Ⅎ 𝑦 𝑋
10 nfmpt1 ⊢ Ⅎ 𝑦 ( 𝑦 ∈ 𝑌 ↦ 𝐴 )
11 9 10 nfmpt ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
12 nfcv ⊢ Ⅎ 𝑦 𝑤
13 11 12 nffv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 )
14 nfcv ⊢ Ⅎ 𝑦 𝑘
15 13 14 nffv ⊢ Ⅎ 𝑦 ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 )
16 nfcv ⊢ Ⅎ 𝑤 ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 )
17 nfcv ⊢ Ⅎ 𝑘 ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 )
18 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) )
19 18 fveq1d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑘 ) )
20 fveq2 ⊢ ( 𝑘 = 𝑦 → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑘 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 ) )
21 19 20 sylan9eq ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑘 = 𝑦 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 ) )
22 8 15 16 17 21 cbvmpo ⊢ ( 𝑤 ∈ 𝑋 , 𝑘 ∈ 𝑌 ↦ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 ) )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
24 nllytop ⊢ ( 𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top )
25 4 24 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
26 topontop ⊢ ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) → 𝐿 ∈ Top )
27 3 26 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
28 eqid ⊢ ( 𝐿 ↑ko 𝐾 ) = ( 𝐿 ↑ko 𝐾 )
29 28 xkotopon ⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
30 25 27 29 syl2anc ⊢ ( 𝜑 → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
31 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
32 1 30 5 31 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
33 32 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) )
35 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
36 35 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
37 23 34 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
38 37 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑦 ) )
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
40 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
41 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
42 cnf2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ 𝑍 )
43 40 41 33 42 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ 𝑍 )
44 43 fvmptelrn ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑍 )
45 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 )
46 45 fvmpt2 ⊢ ( ( 𝑦 ∈ 𝑌 ∧ 𝐴 ∈ 𝑍 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑦 ) = 𝐴 )
47 39 44 46 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑦 ) = 𝐴 )
48 38 47 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 ) = 𝐴 )
49 48 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 ) = 𝐴 )
50 49 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑥 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
51 22 50 syl5eq ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 , 𝑘 ∈ 𝑌 ↦ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
52 1 2 cnmpt1st ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 , 𝑘 ∈ 𝑌 ↦ 𝑤 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
53 1 2 52 5 cnmpt21f ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 , 𝑘 ∈ 𝑌 ↦ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐿 ↑ko 𝐾 ) ) )
54 1 2 cnmpt2nd ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 , 𝑘 ∈ 𝑌 ↦ 𝑘 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
55 eqid ⊢ ( 𝐾 Cn 𝐿 ) = ( 𝐾 Cn 𝐿 )
56 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
57 2 56 syl ⊢ ( 𝜑 → 𝑌 = ∪ 𝐾 )
58 mpoeq12 ⊢ ( ( ( 𝐾 Cn 𝐿 ) = ( 𝐾 Cn 𝐿 ) ∧ 𝑌 = ∪ 𝐾 ) → ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ 𝑌 ↦ ( 𝑓 ‘ 𝑧 ) ) = ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ ∪ 𝐾 ↦ ( 𝑓 ‘ 𝑧 ) ) )
59 55 57 58 sylancr ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ 𝑌 ↦ ( 𝑓 ‘ 𝑧 ) ) = ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ ∪ 𝐾 ↦ ( 𝑓 ‘ 𝑧 ) ) )
60 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
61 eqid ⊢ ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ ∪ 𝐾 ↦ ( 𝑓 ‘ 𝑧 ) ) = ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ ∪ 𝐾 ↦ ( 𝑓 ‘ 𝑧 ) )
62 60 61 xkofvcn ⊢ ( ( 𝐾 ∈ 𝑛-Locally Comp ∧ 𝐿 ∈ Top ) → ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ ∪ 𝐾 ↦ ( 𝑓 ‘ 𝑧 ) ) ∈ ( ( ( 𝐿 ↑ko 𝐾 ) ×t 𝐾 ) Cn 𝐿 ) )
63 4 27 62 syl2anc ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ ∪ 𝐾 ↦ ( 𝑓 ‘ 𝑧 ) ) ∈ ( ( ( 𝐿 ↑ko 𝐾 ) ×t 𝐾 ) Cn 𝐿 ) )
64 59 63 eqeltrd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) , 𝑧 ∈ 𝑌 ↦ ( 𝑓 ‘ 𝑧 ) ) ∈ ( ( ( 𝐿 ↑ko 𝐾 ) ×t 𝐾 ) Cn 𝐿 ) )
65 fveq1 ⊢ ( 𝑓 = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) → ( 𝑓 ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑧 ) )
66 fveq2 ⊢ ( 𝑧 = 𝑘 → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 ) )
67 65 66 sylan9eq ⊢ ( ( 𝑓 = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ∧ 𝑧 = 𝑘 ) → ( 𝑓 ‘ 𝑧 ) = ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 ) )
68 1 2 53 54 30 2 64 67 cnmpt22 ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 , 𝑘 ∈ 𝑌 ↦ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ 𝑤 ) ‘ 𝑘 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
69 51 68 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )