cnmpt1k

Description: The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-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)$
	cnmpt1k.m	$⊢ φ \to M \in TopOn (W)$
	cnmpt1k.a	$⊢ φ \to (x \in X ⟼ A) \in (J Cn L)$
	cnmpt1k.b	$⊢ φ \to (y \in Y ⟼ (z \in Z ⟼ B)) \in (K Cn (M^_{ko} L))$
	cnmpt1k.c	$⊢ z = A \to B = C$
Assertion	cnmpt1k	$⊢ φ \to (y \in Y ⟼ (x \in X ⟼ C)) \in (K Cn (M^_{ko} J))$

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

Metamath Proof Explorer

Theorem cnmpt1k

Proof