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	$⊢ φ \to J \in TopOn (X)$
	cnmptk1p.k	$⊢ φ \to K \in TopOn (Y)$
	cnmptk1p.l	$⊢ φ \to L \in TopOn (Z)$
	cnmptk1p.n	$⊢ φ \to K \in N-LocallyComp$
	cnmptk2.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
Assertion	cnmptk2	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$

Proof

Step	Hyp	Ref	Expression
1		cnmptk1p.j	$⊢ φ \to J \in TopOn (X)$
2		cnmptk1p.k	$⊢ φ \to K \in TopOn (Y)$
3		cnmptk1p.l	$⊢ φ \to L \in TopOn (Z)$
4		cnmptk1p.n	$⊢ φ \to K \in N-LocallyComp$
5		cnmptk2.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
6		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ (y \in Y ⟼ A)) (w)$
7		nfcv	$⊢ \underline{Ⅎ} x k$
8	6 7	nffv	$⊢ \underline{Ⅎ} x (x \in X ⟼ (y \in Y ⟼ A)) (w) (k)$
9		nfcv	$⊢ \underline{Ⅎ} y X$
10		nfmpt1	$⊢ \underline{Ⅎ} y (y \in Y ⟼ A)$
11	9 10	nfmpt	$⊢ \underline{Ⅎ} y (x \in X ⟼ (y \in Y ⟼ A))$
12		nfcv	$⊢ \underline{Ⅎ} y w$
13	11 12	nffv	$⊢ \underline{Ⅎ} y (x \in X ⟼ (y \in Y ⟼ A)) (w)$
14		nfcv	$⊢ \underline{Ⅎ} y k$
15	13 14	nffv	$⊢ \underline{Ⅎ} y (x \in X ⟼ (y \in Y ⟼ A)) (w) (k)$
16		nfcv	$⊢ \underline{Ⅎ} w (x \in X ⟼ (y \in Y ⟼ A)) (x) (y)$
17		nfcv	$⊢ \underline{Ⅎ} k (x \in X ⟼ (y \in Y ⟼ A)) (x) (y)$
18		fveq2	$⊢ w = x \to (x \in X ⟼ (y \in Y ⟼ A)) (w) = (x \in X ⟼ (y \in Y ⟼ A)) (x)$
19	18	fveq1d	$⊢ w = x \to (x \in X ⟼ (y \in Y ⟼ A)) (w) (k) = (x \in X ⟼ (y \in Y ⟼ A)) (x) (k)$
20		fveq2	$⊢ k = y \to (x \in X ⟼ (y \in Y ⟼ A)) (x) (k) = (x \in X ⟼ (y \in Y ⟼ A)) (x) (y)$
21	19 20	sylan9eq	$⊢ (w = x \land k = y) \to (x \in X ⟼ (y \in Y ⟼ A)) (w) (k) = (x \in X ⟼ (y \in Y ⟼ A)) (x) (y)$
22	8 15 16 17 21	cbvmpo	$⊢ (w \in X, k \in Y ⟼ (x \in X ⟼ (y \in Y ⟼ A)) (w) (k)) = (x \in X, y \in Y ⟼ (x \in X ⟼ (y \in Y ⟼ A)) (x) (y))$
23		simplr	$⊢ ((φ \land x \in X) \land y \in Y) \to x \in X$
24		nllytop	$⊢ K \in N-LocallyComp\toK \in Top$
25	4 24	syl	$⊢ φ \to K \in Top$
26		topontop	$⊢ L \in TopOn (Z) \to L \in Top$
27	3 26	syl	$⊢ φ \to L \in Top$
28		eqid	$⊢ L^_{ko} K = L^_{ko} K$
29	28	xkotopon	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in TopOn (K Cn L)$
30	25 27 29	syl2anc	$⊢ φ \to L^_{ko} K \in TopOn (K Cn L)$
31		cnf2	$⊢ (J \in TopOn (X) \land L^_{ko} K \in TopOn (K Cn L) \land (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))) \to (x \in X ⟼ (y \in Y ⟼ A)) : X ⟶ K Cn L$
32	1 30 5 31	syl3anc	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) : X ⟶ K Cn L$
33	32	fvmptelrn	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) \in (K Cn L)$
34	33	adantr	$⊢ ((φ \land x \in X) \land y \in Y) \to (y \in Y ⟼ A) \in (K Cn L)$
35		eqid	$⊢ (x \in X ⟼ (y \in Y ⟼ A)) = (x \in X ⟼ (y \in Y ⟼ A))$
36	35	fvmpt2	$⊢ (x \in X \land (y \in Y ⟼ A) \in (K Cn L)) \to (x \in X ⟼ (y \in Y ⟼ A)) (x) = (y \in Y ⟼ A)$
37	23 34 36	syl2anc	$⊢ ((φ \land x \in X) \land y \in Y) \to (x \in X ⟼ (y \in Y ⟼ A)) (x) = (y \in Y ⟼ A)$
38	37	fveq1d	$⊢ ((φ \land x \in X) \land y \in Y) \to (x \in X ⟼ (y \in Y ⟼ A)) (x) (y) = (y \in Y ⟼ A) (y)$
39		simpr	$⊢ ((φ \land x \in X) \land y \in Y) \to y \in Y$
40	2	adantr	$⊢ (φ \land x \in X) \to K \in TopOn (Y)$
41	3	adantr	$⊢ (φ \land x \in X) \to L \in TopOn (Z)$
42		cnf2	$⊢ (K \in TopOn (Y) \land L \in TopOn (Z) \land (y \in Y ⟼ A) \in (K Cn L)) \to (y \in Y ⟼ A) : Y ⟶ Z$
43	40 41 33 42	syl3anc	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) : Y ⟶ Z$
44	43	fvmptelrn	$⊢ ((φ \land x \in X) \land y \in Y) \to A \in Z$
45		eqid	$⊢ (y \in Y ⟼ A) = (y \in Y ⟼ A)$
46	45	fvmpt2	$⊢ (y \in Y \land A \in Z) \to (y \in Y ⟼ A) (y) = A$
47	39 44 46	syl2anc	$⊢ ((φ \land x \in X) \land y \in Y) \to (y \in Y ⟼ A) (y) = A$
48	38 47	eqtrd	$⊢ ((φ \land x \in X) \land y \in Y) \to (x \in X ⟼ (y \in Y ⟼ A)) (x) (y) = A$
49	48	3impa	$⊢ (φ \land x \in X \land y \in Y) \to (x \in X ⟼ (y \in Y ⟼ A)) (x) (y) = A$
50	49	mpoeq3dva	$⊢ φ \to (x \in X, y \in Y ⟼ (x \in X ⟼ (y \in Y ⟼ A)) (x) (y)) = (x \in X, y \in Y ⟼ A)$
51	22 50	syl5eq	$⊢ φ \to (w \in X, k \in Y ⟼ (x \in X ⟼ (y \in Y ⟼ A)) (w) (k)) = (x \in X, y \in Y ⟼ A)$
52	1 2	cnmpt1st	$⊢ φ \to (w \in X, k \in Y ⟼ w) \in ((J \times_{t} K) Cn J)$
53	1 2 52 5	cnmpt21f	$⊢ φ \to (w \in X, k \in Y ⟼ (x \in X ⟼ (y \in Y ⟼ A)) (w)) \in ((J \times_{t} K) Cn (L^_{ko} K))$
54	1 2	cnmpt2nd	$⊢ φ \to (w \in X, k \in Y ⟼ k) \in ((J \times_{t} K) Cn K)$
55		eqid	$⊢ K Cn L = K Cn L$
56		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
57	2 56	syl	$⊢ φ \to Y = ⋃ K$
58		mpoeq12	$⊢ (K Cn L = K Cn L \land Y = ⋃ K) \to (f \in (K Cn L), z \in Y ⟼ f (z)) = (f \in (K Cn L), z \in ⋃ K ⟼ f (z))$
59	55 57 58	sylancr	$⊢ φ \to (f \in (K Cn L), z \in Y ⟼ f (z)) = (f \in (K Cn L), z \in ⋃ K ⟼ f (z))$
60		eqid	$⊢ ⋃ K = ⋃ K$
61		eqid	$⊢ (f \in (K Cn L), z \in ⋃ K ⟼ f (z)) = (f \in (K Cn L), z \in ⋃ K ⟼ f (z))$
62	60 61	xkofvcn	$⊢ (K \in N-LocallyComp\landL \in Top\to(f \in (K Cn L), z \in ⋃ K ⟼ f (z)) \in (((L^_{ko} K) \times_{t} K) Cn L))$
63	4 27 62	syl2anc	$⊢ φ \to (f \in (K Cn L), z \in ⋃ K ⟼ f (z)) \in (((L^_{ko} K) \times_{t} K) Cn L)$
64	59 63	eqeltrd	$⊢ φ \to (f \in (K Cn L), z \in Y ⟼ f (z)) \in (((L^_{ko} K) \times_{t} K) Cn L)$
65		fveq1	$⊢ f = (x \in X ⟼ (y \in Y ⟼ A)) (w) \to f (z) = (x \in X ⟼ (y \in Y ⟼ A)) (w) (z)$
66		fveq2	$⊢ z = k \to (x \in X ⟼ (y \in Y ⟼ A)) (w) (z) = (x \in X ⟼ (y \in Y ⟼ A)) (w) (k)$
67	65 66	sylan9eq	$⊢ (f = (x \in X ⟼ (y \in Y ⟼ A)) (w) \land z = k) \to f (z) = (x \in X ⟼ (y \in Y ⟼ A)) (w) (k)$
68	1 2 53 54 30 2 64 67	cnmpt22	$⊢ φ \to (w \in X, k \in Y ⟼ (x \in X ⟼ (y \in Y ⟼ A)) (w) (k)) \in ((J \times_{t} K) Cn L)$
69	51 68	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((J \times_{t} K) Cn L)$

Metamath Proof Explorer

Theorem cnmptk2

Proof