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

Definition df-xko 20356
 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 t
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-xko
StepHypRef Expression
1 cxko 20354 . 2
2 vs . . 3
3 vr . . 3
4 ctop 19686 . . 3
5 vk . . . . . . 7
6 vv . . . . . . 7
73cv 1404 . . . . . . . . . 10
8 vx . . . . . . . . . . 11
98cv 1404 . . . . . . . . . 10
10 crest 15035 . . . . . . . . . 10 t
117, 9, 10co 6278 . . . . . . . . 9 t
12 ccmp 20179 . . . . . . . . 9
1311, 12wcel 1842 . . . . . . . 8 t
147cuni 4191 . . . . . . . . 9
1514cpw 3955 . . . . . . . 8
1613, 8, 15crab 2758 . . . . . . 7 t
172cv 1404 . . . . . . 7
18 vf . . . . . . . . . . 11
1918cv 1404 . . . . . . . . . 10
205cv 1404 . . . . . . . . . 10
2119, 20cima 4826 . . . . . . . . 9
226cv 1404 . . . . . . . . 9
2321, 22wss 3414 . . . . . . . 8
24 ccn 20018 . . . . . . . . 9
257, 17, 24co 6278 . . . . . . . 8
2623, 18, 25crab 2758 . . . . . . 7
275, 6, 16, 17, 26cmpt2 6280 . . . . . 6 t
2827crn 4824 . . . . 5 t
29 cfi 7904 . . . . 5
3028, 29cfv 5569 . . . 4 t
31 ctg 15052 . . . 4
3230, 31cfv 5569 . . 3 t
332, 3, 4, 4, 32cmpt2 6280 . 2 t
341, 33wceq 1405 1 t
 Colors of variables: wff setvar class This definition is referenced by:  xkoval  20380
 Copyright terms: Public domain W3C validator