MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xko Unicode version

Definition df-xko 17258
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.)
Assertion
Ref Expression
df-xko  |-  ^ k o  =  ( s  e.  Top ,  r  e. 
Top  |->  ( topGen `  ( fi `  ran  ( k  e.  { x  e. 
~P U. r  |  ( rt  x )  e.  Comp } ,  v  e.  s 
|->  { f  e.  ( r  Cn  s )  |  ( f "
k )  C_  v } ) ) ) )
Distinct variable group:    f, k, r, s, v, x

Detailed syntax breakdown of Definition df-xko
StepHypRef Expression
1 cxko 17256 . 2  class  ^ k o
2 vs . . 3  set  s
3 vr . . 3  set  r
4 ctop 16631 . . 3  class  Top
5 vk . . . . . . 7  set  k
6 vv . . . . . . 7  set  v
73cv 1622 . . . . . . . . . 10  class  r
8 vx . . . . . . . . . . 11  set  x
98cv 1622 . . . . . . . . . 10  class  x
10 crest 13325 . . . . . . . . . 10  classt
117, 9, 10co 5858 . . . . . . . . 9  class  ( rt  x )
12 ccmp 17113 . . . . . . . . 9  class  Comp
1311, 12wcel 1684 . . . . . . . 8  wff  ( rt  x )  e.  Comp
147cuni 3827 . . . . . . . . 9  class  U. r
1514cpw 3625 . . . . . . . 8  class  ~P U. r
1613, 8, 15crab 2547 . . . . . . 7  class  { x  e.  ~P U. r  |  ( rt  x )  e.  Comp }
172cv 1622 . . . . . . 7  class  s
18 vf . . . . . . . . . . 11  set  f
1918cv 1622 . . . . . . . . . 10  class  f
205cv 1622 . . . . . . . . . 10  class  k
2119, 20cima 4692 . . . . . . . . 9  class  ( f
" k )
226cv 1622 . . . . . . . . 9  class  v
2321, 22wss 3152 . . . . . . . 8  wff  ( f
" k )  C_  v
24 ccn 16954 . . . . . . . . 9  class  Cn
257, 17, 24co 5858 . . . . . . . 8  class  ( r  Cn  s )
2623, 18, 25crab 2547 . . . . . . 7  class  { f  e.  ( r  Cn  s )  |  ( f " k ) 
C_  v }
275, 6, 16, 17, 26cmpt2 5860 . . . . . 6  class  ( k  e.  { x  e. 
~P U. r  |  ( rt  x )  e.  Comp } ,  v  e.  s 
|->  { f  e.  ( r  Cn  s )  |  ( f "
k )  C_  v } )
2827crn 4690 . . . . 5  class  ran  (
k  e.  { x  e.  ~P U. r  |  ( rt  x )  e.  Comp } ,  v  e.  s 
|->  { f  e.  ( r  Cn  s )  |  ( f "
k )  C_  v } )
29 cfi 7164 . . . . 5  class  fi
3028, 29cfv 5255 . . . 4  class  ( fi
`  ran  ( k  e.  { x  e.  ~P U. r  |  ( rt  x )  e.  Comp } , 
v  e.  s  |->  { f  e.  ( r  Cn  s )  |  ( f " k
)  C_  v }
) )
31 ctg 13342 . . . 4  class  topGen
3230, 31cfv 5255 . . 3  class  ( topGen `  ( fi `  ran  ( k  e.  {
x  e.  ~P U. r  |  ( rt  x
)  e.  Comp } , 
v  e.  s  |->  { f  e.  ( r  Cn  s )  |  ( f " k
)  C_  v }
) ) )
332, 3, 4, 4, 32cmpt2 5860 . 2  class  ( s  e.  Top ,  r  e.  Top  |->  ( topGen `  ( fi `  ran  ( k  e.  {
x  e.  ~P U. r  |  ( rt  x
)  e.  Comp } , 
v  e.  s  |->  { f  e.  ( r  Cn  s )  |  ( f " k
)  C_  v }
) ) ) )
341, 33wceq 1623 1  wff  ^ k o  =  ( s  e.  Top ,  r  e. 
Top  |->  ( topGen `  ( fi `  ran  ( k  e.  { x  e. 
~P U. r  |  ( rt  x )  e.  Comp } ,  v  e.  s 
|->  { f  e.  ( r  Cn  s )  |  ( f "
k )  C_  v } ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  xkoval  17282
  Copyright terms: Public domain W3C validator