cnmptk1

Description: The composition of a curried function with a one-arg function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cnmptk1.j	$⊢ φ \to J \in TopOn (X)$
2		cnmptk1.k	$⊢ φ \to K \in TopOn (Y)$
3		cnmptk1.l	$⊢ φ \to L \in TopOn (Z)$
4		cnmptk1.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
5		cnmptk1.b	$⊢ φ \to (z \in Z ⟼ B) \in (L Cn M)$
6		cnmptk1.c	$⊢ z = A \to B = C$
7	2	adantr	$⊢ (φ \land x \in X) \to K \in TopOn (Y)$
8	3	adantr	$⊢ (φ \land x \in X) \to L \in TopOn (Z)$
9		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
10	2 9	syl	$⊢ φ \to K \in Top$
11		topontop	$⊢ L \in TopOn (Z) \to L \in Top$
12	3 11	syl	$⊢ φ \to L \in Top$
13		eqid	$⊢ L^_{ko} K = L^_{ko} K$
14	13	xkotopon	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in TopOn (K Cn L)$
15	10 12 14	syl2anc	$⊢ φ \to L^_{ko} K \in TopOn (K Cn L)$
16		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$
17	1 15 4 16	syl3anc	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) : X ⟶ K Cn L$
18	17	fvmptelcdm	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) \in (K Cn L)$
19		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$
20	7 8 18 19	syl3anc	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) : Y ⟶ Z$
21		eqid	$⊢ (y \in Y ⟼ A) = (y \in Y ⟼ A)$
22	21	fmpt	$⊢ \forall y \in Y A \in Z \leftrightarrow (y \in Y ⟼ A) : Y ⟶ Z$
23	20 22	sylibr	$⊢ (φ \land x \in X) \to \forall y \in Y A \in Z$
24		eqidd	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) = (y \in Y ⟼ A)$
25		eqidd	$⊢ (φ \land x \in X) \to (z \in Z ⟼ B) = (z \in Z ⟼ B)$
26	23 24 25 6	fmptcof	$⊢ (φ \land x \in X) \to (z \in Z ⟼ B) \circ (y \in Y ⟼ A) = (y \in Y ⟼ C)$
27	26	mpteq2dva	$⊢ φ \to (x \in X ⟼ (z \in Z ⟼ B) \circ (y \in Y ⟼ A)) = (x \in X ⟼ (y \in Y ⟼ C))$
28	10 5	xkoco2cn	$⊢ φ \to (w \in (K Cn L) ⟼ (z \in Z ⟼ B) \circ w) \in ((L^_{ko} K) Cn (M^_{ko} K))$
29		coeq2	$⊢ w = (y \in Y ⟼ A) \to (z \in Z ⟼ B) \circ w = (z \in Z ⟼ B) \circ (y \in Y ⟼ A)$
30	1 4 15 28 29	cnmpt11	$⊢ φ \to (x \in X ⟼ (z \in Z ⟼ B) \circ (y \in Y ⟼ A)) \in (J Cn (M^_{ko} K))$
31	27 30	eqeltrrd	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ C)) \in (J Cn (M^_{ko} K))$

Metamath Proof Explorer

Theorem cnmptk1

Proof