cnmpt2k

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

	Ref	Expression
Hypotheses	cnmpt2k.j	$⊢ φ \to J \in TopOn (X)$
	cnmpt2k.k	$⊢ φ \to K \in TopOn (Y)$
	cnmpt2k.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
Assertion	cnmpt2k	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$

Proof

Step	Hyp	Ref	Expression
1		cnmpt2k.j	$⊢ φ \to J \in TopOn (X)$
2		cnmpt2k.k	$⊢ φ \to K \in TopOn (Y)$
3		cnmpt2k.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$
4		nfcv	$⊢ \underline{Ⅎ} x Y$
5		nfcv	$⊢ \underline{Ⅎ} x v$
6		nfmpo2	$⊢ \underline{Ⅎ} x (y \in Y, x \in X ⟼ A)$
7		nfcv	$⊢ \underline{Ⅎ} x w$
8	5 6 7	nfov	$⊢ \underline{Ⅎ} x (v (y \in Y, x \in X ⟼ A) w)$
9	4 8	nfmpt	$⊢ \underline{Ⅎ} x (v \in Y ⟼ v (y \in Y, x \in X ⟼ A) w)$
10		nfcv	$⊢ \underline{Ⅎ} w (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) x)$
11		nfcv	$⊢ \underline{Ⅎ} y v$
12		nfmpo1	$⊢ \underline{Ⅎ} y (y \in Y, x \in X ⟼ A)$
13		nfcv	$⊢ \underline{Ⅎ} y w$
14	11 12 13	nfov	$⊢ \underline{Ⅎ} y (v (y \in Y, x \in X ⟼ A) w)$
15		nfcv	$⊢ \underline{Ⅎ} v (y (y \in Y, x \in X ⟼ A) w)$
16		oveq1	$⊢ v = y \to v (y \in Y, x \in X ⟼ A) w = y (y \in Y, x \in X ⟼ A) w$
17	14 15 16	cbvmpt	$⊢ (v \in Y ⟼ v (y \in Y, x \in X ⟼ A) w) = (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) w)$
18		oveq2	$⊢ w = x \to y (y \in Y, x \in X ⟼ A) w = y (y \in Y, x \in X ⟼ A) x$
19	18	mpteq2dv	$⊢ w = x \to (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) w) = (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) x)$
20	17 19	syl5eq	$⊢ w = x \to (v \in Y ⟼ v (y \in Y, x \in X ⟼ A) w) = (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) x)$
21	9 10 20	cbvmpt	$⊢ (w \in X ⟼ (v \in Y ⟼ v (y \in Y, x \in X ⟼ A) w)) = (x \in X ⟼ (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) x))$
22		simpr	$⊢ ((φ \land x \in X) \land y \in Y) \to y \in Y$
23		simplr	$⊢ ((φ \land x \in X) \land y \in Y) \to x \in X$
24		txtopon	$⊢ (K \in TopOn (Y) \land J \in TopOn (X)) \to K \times_{t} J \in TopOn (Y \times X)$
25	2 1 24	syl2anc	$⊢ φ \to K \times_{t} J \in TopOn (Y \times X)$
26		cntop2	$⊢ (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L) \to L \in Top$
27	3 26	syl	$⊢ φ \to L \in Top$
28		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
29	27 28	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
30	1 2 3	cnmptcom	$⊢ φ \to (y \in Y, x \in X ⟼ A) \in ((K \times_{t} J) Cn L)$
31		cnf2	$⊢ (K \times_{t} J \in TopOn (Y \times X) \land L \in TopOn (⋃ L) \land (y \in Y, x \in X ⟼ A) \in ((K \times_{t} J) Cn L)) \to (y \in Y, x \in X ⟼ A) : Y \times X ⟶ ⋃ L$
32	25 29 30 31	syl3anc	$⊢ φ \to (y \in Y, x \in X ⟼ A) : Y \times X ⟶ ⋃ L$
33		eqid	$⊢ (y \in Y, x \in X ⟼ A) = (y \in Y, x \in X ⟼ A)$
34	33	fmpo	$⊢ \forall y \in Y \forall x \in X A \in ⋃ L \leftrightarrow (y \in Y, x \in X ⟼ A) : Y \times X ⟶ ⋃ L$
35	32 34	sylibr	$⊢ φ \to \forall y \in Y \forall x \in X A \in ⋃ L$
36	35	r19.21bi	$⊢ (φ \land y \in Y) \to \forall x \in X A \in ⋃ L$
37	36	r19.21bi	$⊢ ((φ \land y \in Y) \land x \in X) \to A \in ⋃ L$
38	37	an32s	$⊢ ((φ \land x \in X) \land y \in Y) \to A \in ⋃ L$
39	33	ovmpt4g	$⊢ (y \in Y \land x \in X \land A \in ⋃ L) \to y (y \in Y, x \in X ⟼ A) x = A$
40	22 23 38 39	syl3anc	$⊢ ((φ \land x \in X) \land y \in Y) \to y (y \in Y, x \in X ⟼ A) x = A$
41	40	mpteq2dva	$⊢ (φ \land x \in X) \to (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) x) = (y \in Y ⟼ A)$
42	41	mpteq2dva	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ y (y \in Y, x \in X ⟼ A) x)) = (x \in X ⟼ (y \in Y ⟼ A))$
43	21 42	syl5eq	$⊢ φ \to (w \in X ⟼ (v \in Y ⟼ v (y \in Y, x \in X ⟼ A) w)) = (x \in X ⟼ (y \in Y ⟼ A))$
44		eqid	$⊢ (w \in X ⟼ (v \in Y ⟼ ⟨v, w⟩)) = (w \in X ⟼ (v \in Y ⟼ ⟨v, w⟩))$
45	44	xkoinjcn	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (w \in X ⟼ (v \in Y ⟼ ⟨v, w⟩)) \in (J Cn ((K \times_{t} J)^_{ko} K))$
46	1 2 45	syl2anc	$⊢ φ \to (w \in X ⟼ (v \in Y ⟼ ⟨v, w⟩)) \in (J Cn ((K \times_{t} J)^_{ko} K))$
47	32	feqmptd	$⊢ φ \to (y \in Y, x \in X ⟼ A) = (z \in (Y \times X) ⟼ (y \in Y, x \in X ⟼ A) (z))$
48	47 30	eqeltrrd	$⊢ φ \to (z \in (Y \times X) ⟼ (y \in Y, x \in X ⟼ A) (z)) \in ((K \times_{t} J) Cn L)$
49		fveq2	$⊢ z = ⟨v, w⟩ \to (y \in Y, x \in X ⟼ A) (z) = (y \in Y, x \in X ⟼ A) (⟨v, w⟩)$
50		df-ov	$⊢ v (y \in Y, x \in X ⟼ A) w = (y \in Y, x \in X ⟼ A) (⟨v, w⟩)$
51	49 50	eqtr4di	$⊢ z = ⟨v, w⟩ \to (y \in Y, x \in X ⟼ A) (z) = v (y \in Y, x \in X ⟼ A) w$
52	1 2 25 46 48 51	cnmptk1	$⊢ φ \to (w \in X ⟼ (v \in Y ⟼ v (y \in Y, x \in X ⟼ A) w)) \in (J Cn (L^_{ko} K))$
53	43 52	eqeltrrd	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$

Metamath Proof Explorer

Theorem cnmpt2k

Proof