xkofvcn

Description: Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn .) (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	xkofvcn.1	$⊢ X = ⋃ R$
	xkofvcn.2	$⊢ F = (f \in (R Cn S), x \in X ⟼ f (x))$
Assertion	xkofvcn	$⊢ (R \in N-LocallyComp\landS \in Top\toF \in (((S^_{ko} R) \times_{t} R) Cn S))$

Proof

Step	Hyp	Ref	Expression
1		xkofvcn.1	$⊢ X = ⋃ R$
2		xkofvcn.2	$⊢ F = (f \in (R Cn S), x \in X ⟼ f (x))$
3		nllytop	$⊢ R \in N-LocallyComp\toR \in Top$
4		eqid	$⊢ S^_{ko} R = S^_{ko} R$
5	4	xkotopon	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in TopOn (R Cn S)$
6	3 5	sylan	$⊢ (R \in N-LocallyComp\landS \in Top\toS^_{ko} R \in TopOn (R Cn S))$
7	3	adantr	$⊢ (R \in N-LocallyComp\landS \in Top\toR \in Top)$
8	1	toptopon	$⊢ R \in Top \leftrightarrow R \in TopOn (X)$
9	7 8	sylib	$⊢ (R \in N-LocallyComp\landS \in Top\toR \in TopOn (X))$
10	6 9	cnmpt1st	$⊢ (R \in N-LocallyComp\landS \in Top\to(f \in (R Cn S), x \in X ⟼ f) \in (((S^_{ko} R) \times_{t} R) Cn (S^_{ko} R)))$
11	6 9	cnmpt2nd	$⊢ (R \in N-LocallyComp\landS \in Top\to(f \in (R Cn S), x \in X ⟼ x) \in (((S^_{ko} R) \times_{t} R) Cn R))$
12		1on	$⊢ 1_{𝑜} \in On$
13		distopon	$⊢ 1_{𝑜} \in On \to 𝒫 1_{𝑜} \in TopOn (1_{𝑜})$
14	12 13	mp1i	$⊢ (R \in N-LocallyComp\landS \in Top\to𝒫 1_{𝑜} \in TopOn (1_{𝑜}))$
15		xkoccn	$⊢ (𝒫 1_{𝑜} \in TopOn (1_{𝑜}) \land R \in TopOn (X)) \to (y \in X ⟼ 1_{𝑜} \times \{y\}) \in (R Cn (R^_{ko} 𝒫 1_{𝑜}))$
16	14 9 15	syl2anc	$⊢ (R \in N-LocallyComp\landS \in Top\to(y \in X ⟼ 1_{𝑜} \times \{y\}) \in (R Cn (R^_{ko} 𝒫 1_{𝑜})))$
17		sneq	$⊢ y = x \to \{y\} = \{x\}$
18	17	xpeq2d	$⊢ y = x \to 1_{𝑜} \times \{y\} = 1_{𝑜} \times \{x\}$
19	6 9 11 9 16 18	cnmpt21	$⊢ (R \in N-LocallyComp\landS \in Top\to(f \in (R Cn S), x \in X ⟼ 1_{𝑜} \times \{x\}) \in (((S^_{ko} R) \times_{t} R) Cn (R^_{ko} 𝒫 1_{𝑜})))$
20		distop	$⊢ 1_{𝑜} \in On \to 𝒫 1_{𝑜} \in Top$
21	12 20	mp1i	$⊢ (R \in N-LocallyComp\landS \in Top\to𝒫 1_{𝑜} \in Top)$
22		eqid	$⊢ R^_{ko} 𝒫 1_{𝑜} = R^_{ko} 𝒫 1_{𝑜}$
23	22	xkotopon	$⊢ (𝒫 1_{𝑜} \in Top \land R \in Top) \to R^_{ko} 𝒫 1_{𝑜} \in TopOn (𝒫 1_{𝑜} Cn R)$
24	21 7 23	syl2anc	$⊢ (R \in N-LocallyComp\landS \in Top\toR^_{ko} 𝒫 1_{𝑜} \in TopOn (𝒫 1_{𝑜} Cn R))$
25		simpl	$⊢ (R \in N-LocallyComp\landS \in Top\toR \in N-LocallyComp)$
26		simpr	$⊢ (R \in N-LocallyComp\landS \in Top\toS \in Top)$
27		eqid	$⊢ (g \in (R Cn S), h \in (𝒫 1_{𝑜} Cn R) ⟼ g \circ h) = (g \in (R Cn S), h \in (𝒫 1_{𝑜} Cn R) ⟼ g \circ h)$
28	27	xkococn	$⊢ (𝒫 1_{𝑜} \in Top \land R \in N-LocallyComp\landS \in Top\to(g \in (R Cn S), h \in (𝒫 1_{𝑜} Cn R) ⟼ g \circ h) \in (((S^_{ko} R) \times_{t} (R^_{ko} 𝒫 1_{𝑜})) Cn (S^_{ko} 𝒫 1_{𝑜})))$
29	21 25 26 28	syl3anc	$⊢ (R \in N-LocallyComp\landS \in Top\to(g \in (R Cn S), h \in (𝒫 1_{𝑜} Cn R) ⟼ g \circ h) \in (((S^_{ko} R) \times_{t} (R^_{ko} 𝒫 1_{𝑜})) Cn (S^_{ko} 𝒫 1_{𝑜})))$
30		coeq1	$⊢ g = f \to g \circ h = f \circ h$
31		coeq2	$⊢ h = 1_{𝑜} \times \{x\} \to f \circ h = f \circ (1_{𝑜} \times \{x\})$
32	30 31	sylan9eq	$⊢ (g = f \land h = 1_{𝑜} \times \{x\}) \to g \circ h = f \circ (1_{𝑜} \times \{x\})$
33	6 9 10 19 6 24 29 32	cnmpt22	$⊢ (R \in N-LocallyComp\landS \in Top\to(f \in (R Cn S), x \in X ⟼ f \circ (1_{𝑜} \times \{x\})) \in (((S^_{ko} R) \times_{t} R) Cn (S^_{ko} 𝒫 1_{𝑜})))$
34		eqid	$⊢ S^_{ko} 𝒫 1_{𝑜} = S^_{ko} 𝒫 1_{𝑜}$
35	34	xkotopon	$⊢ (𝒫 1_{𝑜} \in Top \land S \in Top) \to S^_{ko} 𝒫 1_{𝑜} \in TopOn (𝒫 1_{𝑜} Cn S)$
36	21 26 35	syl2anc	$⊢ (R \in N-LocallyComp\landS \in Top\toS^_{ko} 𝒫 1_{𝑜} \in TopOn (𝒫 1_{𝑜} Cn S))$
37		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
38	37	a1i	$⊢ (R \in N-LocallyComp\landS \in Top\to\emptyset \in 1_{𝑜})$
39		unipw	$⊢ ⋃ 𝒫 1_{𝑜} = 1_{𝑜}$
40	39	eqcomi	$⊢ 1_{𝑜} = ⋃ 𝒫 1_{𝑜}$
41	40	xkopjcn	$⊢ (𝒫 1_{𝑜} \in Top \land S \in Top \land \emptyset \in 1_{𝑜}) \to (g \in (𝒫 1_{𝑜} Cn S) ⟼ g (\emptyset)) \in ((S^_{ko} 𝒫 1_{𝑜}) Cn S)$
42	21 26 38 41	syl3anc	$⊢ (R \in N-LocallyComp\landS \in Top\to(g \in (𝒫 1_{𝑜} Cn S) ⟼ g (\emptyset)) \in ((S^_{ko} 𝒫 1_{𝑜}) Cn S))$
43		fveq1	$⊢ g = f \circ (1_{𝑜} \times \{x\}) \to g (\emptyset) = (f \circ (1_{𝑜} \times \{x\})) (\emptyset)$
44		vex	$⊢ x \in V$
45	44	fconst	$⊢ (1_{𝑜} \times \{x\}) : 1_{𝑜} ⟶ \{x\}$
46		fvco3	$⊢ ((1_{𝑜} \times \{x\}) : 1_{𝑜} ⟶ \{x\} \land \emptyset \in 1_{𝑜}) \to (f \circ (1_{𝑜} \times \{x\})) (\emptyset) = f ((1_{𝑜} \times \{x\}) (\emptyset))$
47	45 37 46	mp2an	$⊢ (f \circ (1_{𝑜} \times \{x\})) (\emptyset) = f ((1_{𝑜} \times \{x\}) (\emptyset))$
48	44	fvconst2	$⊢ \emptyset \in 1_{𝑜} \to (1_{𝑜} \times \{x\}) (\emptyset) = x$
49	37 48	ax-mp	$⊢ (1_{𝑜} \times \{x\}) (\emptyset) = x$
50	49	fveq2i	$⊢ f ((1_{𝑜} \times \{x\}) (\emptyset)) = f (x)$
51	47 50	eqtri	$⊢ (f \circ (1_{𝑜} \times \{x\})) (\emptyset) = f (x)$
52	43 51	eqtrdi	$⊢ g = f \circ (1_{𝑜} \times \{x\}) \to g (\emptyset) = f (x)$
53	6 9 33 36 42 52	cnmpt21	$⊢ (R \in N-LocallyComp\landS \in Top\to(f \in (R Cn S), x \in X ⟼ f (x)) \in (((S^_{ko} R) \times_{t} R) Cn S))$
54	2 53	eqeltrid	$⊢ (R \in N-LocallyComp\landS \in Top\toF \in (((S^_{ko} R) \times_{t} R) Cn S))$

Metamath Proof Explorer

Theorem xkofvcn

Proof