This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = U. R
xkoopn.r 
|- ( ph -> R e. Top )
xkoopn.s 
|- ( ph -> S e. Top )
xkoopn.a 
|- ( ph -> A C_ X )
xkoopn.c 
|- ( ph -> ( R |`t A ) e. Comp )
xkoopn.u 
|- ( ph -> U e. S )
Assertion xkoopn 
|- ( ph -> { f e. ( R Cn S ) | ( f " A ) C_ U } e. ( S ^ko R ) )

Proof

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