This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnmpt2k

Description: The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypotheses cnmpt2k.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt2k.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
cnmpt2k.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
Assertion cnmpt2k ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 cnmpt2k.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmpt2k.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmpt2k.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
4 nfcv ⊢ Ⅎ 𝑥 𝑌
5 nfcv ⊢ Ⅎ 𝑥 𝑣
6 nfmpo2 ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 )
7 nfcv ⊢ Ⅎ 𝑥 𝑤
8 5 6 7 nfov ⊢ Ⅎ 𝑥 ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 )
9 4 8 nfmpt ⊢ Ⅎ 𝑥 ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) )
10 nfcv ⊢ Ⅎ 𝑤 ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) )
11 nfcv ⊢ Ⅎ 𝑦 𝑣
12 nfmpo1 ⊢ Ⅎ 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 )
13 nfcv ⊢ Ⅎ 𝑦 𝑤
14 11 12 13 nfov ⊢ Ⅎ 𝑦 ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 )
15 nfcv ⊢ Ⅎ 𝑣 ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 )
16 oveq1 ⊢ ( 𝑣 = 𝑦 → ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) = ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) )
17 14 15 16 cbvmpt ⊢ ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) )
18 oveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) = ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) )
19 18 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) ) )
20 17 19 eqtrid ⊢ ( 𝑤 = 𝑥 → ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) ) )
21 9 10 20 cbvmpt ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) ) )
22 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
24 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐾 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑋 ) ) )
25 2 1 24 syl2anc ⊢ ( 𝜑 → ( 𝐾 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑋 ) ) )
26 cntop2 ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) → 𝐿 ∈ Top )
27 3 26 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
28 toptopon2 ⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
29 27 28 sylib ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
30 1 2 3 cnmptcom ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐿 ) )
31 cnf2 ⊢ ( ( ( 𝐾 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑋 ) ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐿 ) ) → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) : ( 𝑌 × 𝑋 ) ⟶ ∪ 𝐿 )
32 25 29 30 31 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) : ( 𝑌 × 𝑋 ) ⟶ ∪ 𝐿 )
33 eqid ⊢ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 )
34 33 fmpo ⊢ ( ∀ 𝑦 ∈ 𝑌 ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿 ↔ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) : ( 𝑌 × 𝑋 ) ⟶ ∪ 𝐿 )
35 32 34 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿 )
36 35 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿 )
37 36 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ∪ 𝐿 )
38 37 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ∪ 𝐿 )
39 33 ovmpt4g ⊢ ( ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ 𝐿 ) → ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) = 𝐴 )
40 22 23 38 39 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) = 𝐴 )
41 40 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) )
42 41 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) )
43 21 42 eqtrid ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) )
44 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ⟨ 𝑣 , 𝑤 ⟩ ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ⟨ 𝑣 , 𝑤 ⟩ ) )
45 44 xkoinjcn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ⟨ 𝑣 , 𝑤 ⟩ ) ) ∈ ( 𝐽 Cn ( ( 𝐾 ×t 𝐽 ) ↑ko 𝐾 ) ) )
46 1 2 45 syl2anc ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ⟨ 𝑣 , 𝑤 ⟩ ) ) ∈ ( 𝐽 Cn ( ( 𝐾 ×t 𝐽 ) ↑ko 𝐾 ) ) )
47 32 feqmptd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑧 ) ) )
48 47 30 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑧 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐿 ) )
49 fveq2 ⊢ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ → ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑧 ) = ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ ⟨ 𝑣 , 𝑤 ⟩ ) )
50 df-ov ⊢ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) = ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ ⟨ 𝑣 , 𝑤 ⟩ )
51 49 50 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑣 , 𝑤 ⟩ → ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑧 ) = ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) )
52 1 2 25 46 48 51 cnmptk1 ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
53 43 52 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )