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

Definition df-xko 17597
 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 17595 . 2
2 vs . . 3
3 vr . . 3
4 ctop 16960 . . 3
5 vk . . . . . . 7
6 vv . . . . . . 7
73cv 1652 . . . . . . . . . 10
8 vx . . . . . . . . . . 11
98cv 1652 . . . . . . . . . 10
10 crest 13650 . . . . . . . . . 10 t
117, 9, 10co 6083 . . . . . . . . 9 t
12 ccmp 17451 . . . . . . . . 9
1311, 12wcel 1726 . . . . . . . 8 t
147cuni 4017 . . . . . . . . 9
1514cpw 3801 . . . . . . . 8
1613, 8, 15crab 2711 . . . . . . 7 t
172cv 1652 . . . . . . 7
18 vf . . . . . . . . . . 11
1918cv 1652 . . . . . . . . . 10
205cv 1652 . . . . . . . . . 10
2119, 20cima 4883 . . . . . . . . 9
226cv 1652 . . . . . . . . 9
2321, 22wss 3322 . . . . . . . 8
24 ccn 17290 . . . . . . . . 9
257, 17, 24co 6083 . . . . . . . 8
2623, 18, 25crab 2711 . . . . . . 7
275, 6, 16, 17, 26cmpt2 6085 . . . . . 6 t
2827crn 4881 . . . . 5 t
29 cfi 7417 . . . . 5
3028, 29cfv 5456 . . . 4 t
31 ctg 13667 . . . 4
3230, 31cfv 5456 . . 3 t
332, 3, 4, 4, 32cmpt2 6085 . 2 t
341, 33wceq 1653 1 t
 Colors of variables: wff set class This definition is referenced by:  xkoval  17621
 Copyright terms: Public domain W3C validator