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	syl5eq	⊢ ( 𝑤 = 𝑥 → ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑦 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑥 ) ) )
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	syl5eq	⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑣 ∈ 𝑌 ↦ ( 𝑣 ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝐴 ) 𝑤 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) )
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 𝐾 ) ) )