cnmptk1p

Description: The evaluation of a curried function by a one-arg function is jointly 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$
	cnmptk1p.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
	cnmptk1p.b	$⊢ φ \to (x \in X ⟼ B) \in (J Cn K)$
	cnmptk1p.c	$⊢ y = B \to A = C$
Assertion	cnmptk1p	$⊢ φ \to (x \in X ⟼ C) \in (J 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		cnmptk1p.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
6		cnmptk1p.b	$⊢ φ \to (x \in X ⟼ B) \in (J Cn K)$
7		cnmptk1p.c	$⊢ y = B \to A = C$
8		eqid	$⊢ (y \in Y ⟼ A) = (y \in Y ⟼ A)$
9		cnf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land (x \in X ⟼ B) \in (J Cn K)) \to (x \in X ⟼ B) : X ⟶ Y$
10	1 2 6 9	syl3anc	$⊢ φ \to (x \in X ⟼ B) : X ⟶ Y$
11	10	fvmptelrn	$⊢ (φ \land x \in X) \to B \in Y$
12	7	eleq1d	$⊢ y = B \to (A \in Z \leftrightarrow C \in Z)$
13	2	adantr	$⊢ (φ \land x \in X) \to K \in TopOn (Y)$
14	3	adantr	$⊢ (φ \land x \in X) \to L \in TopOn (Z)$
15		nllytop	$⊢ K \in N-LocallyComp\toK \in Top$
16	4 15	syl	$⊢ φ \to K \in Top$
17		topontop	$⊢ L \in TopOn (Z) \to L \in Top$
18	3 17	syl	$⊢ φ \to L \in Top$
19		eqid	$⊢ L^_{ko} K = L^_{ko} K$
20	19	xkotopon	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in TopOn (K Cn L)$
21	16 18 20	syl2anc	$⊢ φ \to L^_{ko} K \in TopOn (K Cn L)$
22		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$
23	1 21 5 22	syl3anc	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) : X ⟶ K Cn L$
24	23	fvmptelrn	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) \in (K Cn L)$
25		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$
26	13 14 24 25	syl3anc	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) : Y ⟶ Z$
27	8	fmpt	$⊢ \forall y \in Y A \in Z \leftrightarrow (y \in Y ⟼ A) : Y ⟶ Z$
28	26 27	sylibr	$⊢ (φ \land x \in X) \to \forall y \in Y A \in Z$
29	12 28 11	rspcdva	$⊢ (φ \land x \in X) \to C \in Z$
30	8 7 11 29	fvmptd3	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) (B) = C$
31	30	mpteq2dva	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A) (B)) = (x \in X ⟼ C)$
32		eqid	$⊢ K Cn L = K Cn L$
33		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
34	2 33	syl	$⊢ φ \to Y = ⋃ K$
35		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))$
36	32 34 35	sylancr	$⊢ φ \to (f \in (K Cn L), z \in Y ⟼ f (z)) = (f \in (K Cn L), z \in ⋃ K ⟼ f (z))$
37		eqid	$⊢ ⋃ K = ⋃ K$
38		eqid	$⊢ (f \in (K Cn L), z \in ⋃ K ⟼ f (z)) = (f \in (K Cn L), z \in ⋃ K ⟼ f (z))$
39	37 38	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))$
40	4 18 39	syl2anc	$⊢ φ \to (f \in (K Cn L), z \in ⋃ K ⟼ f (z)) \in (((L^_{ko} K) \times_{t} K) Cn L)$
41	36 40	eqeltrd	$⊢ φ \to (f \in (K Cn L), z \in Y ⟼ f (z)) \in (((L^_{ko} K) \times_{t} K) Cn L)$
42		fveq1	$⊢ f = (y \in Y ⟼ A) \to f (z) = (y \in Y ⟼ A) (z)$
43		fveq2	$⊢ z = B \to (y \in Y ⟼ A) (z) = (y \in Y ⟼ A) (B)$
44	42 43	sylan9eq	$⊢ (f = (y \in Y ⟼ A) \land z = B) \to f (z) = (y \in Y ⟼ A) (B)$
45	1 5 6 21 2 41 44	cnmpt12	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A) (B)) \in (J Cn L)$
46	31 45	eqeltrrd	$⊢ φ \to (x \in X ⟼ C) \in (J Cn L)$

Metamath Proof Explorer

Theorem cnmptk1p

Proof