cnmptkp

Description: The evaluation of the inner function in 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)$
	cnmptkp.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
	cnmptkp.b	$⊢ φ \to B \in Y$
	cnmptkp.c	$⊢ y = B \to A = C$
Assertion	cnmptkp	$⊢ φ \to (x \in X ⟼ C) \in (J Cn L)$

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		cnmptkp.a	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) \in (J Cn (L^_{ko} K))$
5		cnmptkp.b	$⊢ φ \to B \in Y$
6		cnmptkp.c	$⊢ y = B \to A = C$
7		eqid	$⊢ (y \in Y ⟼ A) = (y \in Y ⟼ A)$
8	5	adantr	$⊢ (φ \land x \in X) \to B \in Y$
9	6	eleq1d	$⊢ y = B \to (A \in ⋃ L \leftrightarrow C \in ⋃ L)$
10	2	adantr	$⊢ (φ \land x \in X) \to K \in TopOn (Y)$
11		topontop	$⊢ L \in TopOn (Z) \to L \in Top$
12	3 11	syl	$⊢ φ \to L \in Top$
13	12	adantr	$⊢ (φ \land x \in X) \to L \in Top$
14		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
15	13 14	sylib	$⊢ (φ \land x \in X) \to L \in TopOn (⋃ L)$
16		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
17	2 16	syl	$⊢ φ \to K \in Top$
18		eqid	$⊢ L^_{ko} K = L^_{ko} K$
19	18	xkotopon	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in TopOn (K Cn L)$
20	17 12 19	syl2anc	$⊢ φ \to L^_{ko} K \in TopOn (K Cn L)$
21		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$
22	1 20 4 21	syl3anc	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A)) : X ⟶ K Cn L$
23	22	fvmptelrn	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) \in (K Cn L)$
24		cnf2	$⊢ (K \in TopOn (Y) \land L \in TopOn (⋃ L) \land (y \in Y ⟼ A) \in (K Cn L)) \to (y \in Y ⟼ A) : Y ⟶ ⋃ L$
25	10 15 23 24	syl3anc	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) : Y ⟶ ⋃ L$
26	7	fmpt	$⊢ \forall y \in Y A \in ⋃ L \leftrightarrow (y \in Y ⟼ A) : Y ⟶ ⋃ L$
27	25 26	sylibr	$⊢ (φ \land x \in X) \to \forall y \in Y A \in ⋃ L$
28	9 27 8	rspcdva	$⊢ (φ \land x \in X) \to C \in ⋃ L$
29	7 6 8 28	fvmptd3	$⊢ (φ \land x \in X) \to (y \in Y ⟼ A) (B) = C$
30	29	mpteq2dva	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A) (B)) = (x \in X ⟼ C)$
31		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
32	2 31	syl	$⊢ φ \to Y = ⋃ K$
33	5 32	eleqtrd	$⊢ φ \to B \in ⋃ K$
34		eqid	$⊢ ⋃ K = ⋃ K$
35	34	xkopjcn	$⊢ (K \in Top \land L \in Top \land B \in ⋃ K) \to (w \in (K Cn L) ⟼ w (B)) \in ((L^_{ko} K) Cn L)$
36	17 12 33 35	syl3anc	$⊢ φ \to (w \in (K Cn L) ⟼ w (B)) \in ((L^_{ko} K) Cn L)$
37		fveq1	$⊢ w = (y \in Y ⟼ A) \to w (B) = (y \in Y ⟼ A) (B)$
38	1 4 20 36 37	cnmpt11	$⊢ φ \to (x \in X ⟼ (y \in Y ⟼ A) (B)) \in (J Cn L)$
39	30 38	eqeltrrd	$⊢ φ \to (x \in X ⟼ C) \in (J Cn L)$

Metamath Proof Explorer

Theorem cnmptkp

Proof