Metamath Proof Explorer


Theorem xkoopn

Description: A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses xkoopn.x X = R
xkoopn.r φ R Top
xkoopn.s φ S Top
xkoopn.a φ A X
xkoopn.c φ R 𝑡 A Comp
xkoopn.u φ U S
Assertion xkoopn φ f R Cn S | f A U S ^ ko R

Proof

Step Hyp Ref Expression
1 xkoopn.x X = R
2 xkoopn.r φ R Top
3 xkoopn.s φ S Top
4 xkoopn.a φ A X
5 xkoopn.c φ R 𝑡 A Comp
6 xkoopn.u φ U S
7 ovex R Cn S V
8 7 pwex 𝒫 R Cn S V
9 eqid x 𝒫 X | R 𝑡 x Comp = x 𝒫 X | R 𝑡 x Comp
10 eqid k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v = k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
11 1 9 10 xkotf k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v : x 𝒫 X | R 𝑡 x Comp × S 𝒫 R Cn S
12 frn k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v : x 𝒫 X | R 𝑡 x Comp × S 𝒫 R Cn S ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v 𝒫 R Cn S
13 11 12 ax-mp ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v 𝒫 R Cn S
14 8 13 ssexi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v V
15 ssfii ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v V ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
16 14 15 ax-mp ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
17 fvex fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v V
18 bastg fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v V fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v topGen fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
19 17 18 ax-mp fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v topGen fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
20 16 19 sstri ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v topGen fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
21 oveq2 x = A R 𝑡 x = R 𝑡 A
22 21 eleq1d x = A R 𝑡 x Comp R 𝑡 A Comp
23 1 topopn R Top X R
24 elpw2g X R A 𝒫 X A X
25 2 23 24 3syl φ A 𝒫 X A X
26 4 25 mpbird φ A 𝒫 X
27 22 26 5 elrabd φ A x 𝒫 X | R 𝑡 x Comp
28 eqidd φ f R Cn S | f A U = f R Cn S | f A U
29 imaeq2 k = A f k = f A
30 29 sseq1d k = A f k v f A v
31 30 rabbidv k = A f R Cn S | f k v = f R Cn S | f A v
32 31 eqeq2d k = A f R Cn S | f A U = f R Cn S | f k v f R Cn S | f A U = f R Cn S | f A v
33 sseq2 v = U f A v f A U
34 33 rabbidv v = U f R Cn S | f A v = f R Cn S | f A U
35 34 eqeq2d v = U f R Cn S | f A U = f R Cn S | f A v f R Cn S | f A U = f R Cn S | f A U
36 32 35 rspc2ev A x 𝒫 X | R 𝑡 x Comp U S f R Cn S | f A U = f R Cn S | f A U k x 𝒫 X | R 𝑡 x Comp v S f R Cn S | f A U = f R Cn S | f k v
37 27 6 28 36 syl3anc φ k x 𝒫 X | R 𝑡 x Comp v S f R Cn S | f A U = f R Cn S | f k v
38 7 rabex f R Cn S | f A U V
39 eqeq1 y = f R Cn S | f A U y = f R Cn S | f k v f R Cn S | f A U = f R Cn S | f k v
40 39 2rexbidv y = f R Cn S | f A U k x 𝒫 X | R 𝑡 x Comp v S y = f R Cn S | f k v k x 𝒫 X | R 𝑡 x Comp v S f R Cn S | f A U = f R Cn S | f k v
41 10 rnmpo ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v = y | k x 𝒫 X | R 𝑡 x Comp v S y = f R Cn S | f k v
42 38 40 41 elab2 f R Cn S | f A U ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v k x 𝒫 X | R 𝑡 x Comp v S f R Cn S | f A U = f R Cn S | f k v
43 37 42 sylibr φ f R Cn S | f A U ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
44 20 43 sseldi φ f R Cn S | f A U topGen fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
45 1 9 10 xkoval R Top S Top S ^ ko R = topGen fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
46 2 3 45 syl2anc φ S ^ ko R = topGen fi ran k x 𝒫 X | R 𝑡 x Comp , v S f R Cn S | f k v
47 44 46 eleqtrrd φ f R Cn S | f A U S ^ ko R