cnmptkk

Description: The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmptkk.j	$⊢ φ \to J \in TopOn (X)$
	cnmptkk.k	$⊢ φ \to K \in TopOn (Y)$
	cnmptkk.l	$⊢ φ \to L \in TopOn (Z)$
	cnmptkk.m	$⊢ φ \to M \in TopOn (W)$
	cnmptkk.n	$⊢ φ \to L \in N-LocallyComp$
	cnmptkk.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
	cnmptkk.b	$⊢ φ \to (x \in X ⟼ (z \in Z ⟼ B)) \in (J Cn (M^_{ko} L))$
	cnmptkk.c	$⊢ z = A \to B = C$
Assertion	cnmptkk	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ C)) \in (J Cn (M^_{ko} K))$

Proof

Step	Hyp	Ref	Expression
1		cnmptkk.j	$⊢ φ \to J \in TopOn (X)$
2		cnmptkk.k	$⊢ φ \to K \in TopOn (Y)$
3		cnmptkk.l	$⊢ φ \to L \in TopOn (Z)$
4		cnmptkk.m	$⊢ φ \to M \in TopOn (W)$
5		cnmptkk.n	$⊢ φ \to L \in N-LocallyComp$
6		cnmptkk.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
7		cnmptkk.b	$⊢ φ \to (x \in X ⟼ (z \in Z ⟼ B)) \in (J Cn (M^_{ko} L))$
8		cnmptkk.c	$⊢ z = A \to B = C$
9	2	adantr	$⊢ (φ \land x \in X) \to K \in TopOn (Y)$
10	3	adantr	$⊢ (φ \land x \in X) \to L \in TopOn (Z)$
11		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
12	2 11	syl	$⊢ φ \to K \in Top$
13		nllytop	$⊢ L \in N-LocallyComp\toL \in Top$
14	5 13	syl	$⊢ φ \to L \in Top$
15		eqid	$⊢ L^_{ko} K = L^_{ko} K$
16	15	xkotopon	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in TopOn (K Cn L)$
17	12 14 16	syl2anc	$⊢ φ \to L^_{ko} K \in TopOn (K Cn L)$
18		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$
19	1 17 6 18	syl3anc	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) : X ⟶ K Cn L$
20	19	fvmptelcdm	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) \in (K Cn L)$
21		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$
22	9 10 20 21	syl3anc	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) : Y ⟶ Z$
23		eqid	$⊢ (y \in Y ⟼ A) = (y \in Y ⟼ A)$
24	23	fmpt	$⊢ \forall y \in Y A \in Z \leftrightarrow (y \in Y ⟼ A) : Y ⟶ Z$
25	22 24	sylibr	$⊢ (φ \land x \in X) \to \forall y \in Y A \in Z$
26		eqidd	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) = (y \in Y ⟼ A)$
27		eqidd	$⊢ (φ \land x \in X) \to (z \in Z ⟼ B) = (z \in Z ⟼ B)$
28	25 26 27 8	fmptcof	$⊢ (φ \land x \in X) \to (z \in Z ⟼ B) \circ (y \in Y ⟼ A) = (y \in Y ⟼ C)$
29	28	mpteq2dva	$⊢ φ \to (x \in X ⟼ (z \in Z ⟼ B) \circ (y \in Y ⟼ A)) = (x \in X ⟼ (y \in Y ⟼ C))$
30		topontop	$⊢ M \in TopOn (W) \to M \in Top$
31	4 30	syl	$⊢ φ \to M \in Top$
32		eqid	$⊢ M^_{ko} L = M^_{ko} L$
33	32	xkotopon	$⊢ (L \in Top \land M \in Top) \to M^_{ko} L \in TopOn (L Cn M)$
34	14 31 33	syl2anc	$⊢ φ \to M^_{ko} L \in TopOn (L Cn M)$
35		eqid	$⊢ (f \in (L Cn M), g \in (K Cn L) ⟼ f \circ g) = (f \in (L Cn M), g \in (K Cn L) ⟼ f \circ g)$
36	35	xkococn	$⊢ (K \in Top \land L \in N-LocallyComp\landM \in Top\to(f \in (L Cn M), g \in (K Cn L) ⟼ f \circ g) \in (((M^_{ko} L) \times_{t} (L^_{ko} K)) Cn (M^_{ko} K)))$
37	12 5 31 36	syl3anc	$⊢ φ \to (f \in (L Cn M), g \in (K Cn L) ⟼ f \circ g) \in (((M^_{ko} L) \times_{t} (L^_{ko} K)) Cn (M^_{ko} K))$
38		coeq1	$⊢ f = (z \in Z ⟼ B) \to f \circ g = (z \in Z ⟼ B) \circ g$
39		coeq2	$⊢ g = (y \in Y ⟼ A) \to (z \in Z ⟼ B) \circ g = (z \in Z ⟼ B) \circ (y \in Y ⟼ A)$
40	38 39	sylan9eq	$⊢ (f = (z \in Z ⟼ B) \land g = (y \in Y ⟼ A)) \to f \circ g = (z \in Z ⟼ B) \circ (y \in Y ⟼ A)$
41	1 7 6 34 17 37 40	cnmpt12	$⊢ φ \to (x \in X ⟼ (z \in Z ⟼ B) \circ (y \in Y ⟼ A)) \in (J Cn (M^_{ko} K))$
42	29 41	eqeltrrd	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ C)) \in (J Cn (M^_{ko} K))$

Metamath Proof Explorer

Theorem cnmptkk

Proof