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

Metamath Proof Explorer

Definition df-xko

Description: Define the compact-open topology, which is the natural topology on the set of continuous functions between two topological spaces. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion df-xko 
|- ^ko = ( s e. Top , r e. Top |-> ( topGen ` ( fi ` ran ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxko 
 |-  ^ko
1 vs 
 |-  s
2 ctop 
 |-  Top
3 vr 
 |-  r
4 ctg 
 |-  topGen
5 cfi 
 |-  fi
6 vk 
 |-  k
7 vx 
 |-  x
8 3 cv 
 |-  r
9 8 cuni 
 |-  U. r
10 9 cpw 
 |-  ~P U. r
11 crest 
 |-  |`t
12 7 cv 
 |-  x
13 8 12 11 co 
 |-  ( r |`t x )
14 ccmp 
 |-  Comp
15 13 14 wcel 
 |-  ( r |`t x ) e. Comp
16 15 7 10 crab 
 |-  { x e. ~P U. r | ( r |`t x ) e. Comp }
17 vv 
 |-  v
18 1 cv 
 |-  s
19 vf 
 |-  f
20 ccn 
 |-  Cn
21 8 18 20 co 
 |-  ( r Cn s )
22 19 cv 
 |-  f
23 6 cv 
 |-  k
24 22 23 cima 
 |-  ( f " k )
25 17 cv 
 |-  v
26 24 25 wss 
 |-  ( f " k ) C_ v
27 26 19 21 crab 
 |-  { f e. ( r Cn s ) | ( f " k ) C_ v }
28 6 17 16 18 27 cmpo 
 |-  ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } )
29 28 crn 
 |-  ran ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } )
30 29 5 cfv 
 |-  ( fi ` ran ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } ) )
31 30 4 cfv 
 |-  ( topGen ` ( fi ` ran ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } ) ) )
32 1 3 2 2 31 cmpo 
 |-  ( s e. Top , r e. Top |-> ( topGen ` ( fi ` ran ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } ) ) ) )
33 0 32 wceq 
 |-  ^ko = ( s e. Top , r e. Top |-> ( topGen ` ( fi ` ran ( k e. { x e. ~P U. r | ( r |`t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } ) ) ) )