# Metamath Proof Explorer

## Theorem 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}=\bigcup {R}$
xkofvcn.2 ${⊢}{F}=\left({f}\in \left({R}\mathrm{Cn}{S}\right),{x}\in {X}⟼{f}\left({x}\right)\right)$
Assertion xkofvcn ${⊢}\left({R}\in N-Locally\mathrm{Comp}\wedge {S}\in \mathrm{Top}\to {F}\in \left(\left(\left({S}{^}_{\mathrm{ko}}{R}\right){×}_{t}{R}\right)\mathrm{Cn}{S}\right)\right)$

### Proof

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