Definition df-xko 21366

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	|- ^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 } ) ) ) )

Distinct variable group:   f, k, r, s, v, x

Detailed syntax breakdown of Definition df-xko

Step	Hyp	Ref	Expression
1		cxko 21364	. 2 class ^ko
2		vs	. . 3 setvar s
3		vr	. . 3 setvar r
4		ctop 20698	. . 3 class Top
5		vk	. . . . . . 7 setvar k
6		vv	. . . . . . 7 setvar v
7	3	cv 1482	. . . . . . . . . 10 class r
8		vx	. . . . . . . . . . 11 setvar x
9	8	cv 1482	. . . . . . . . . 10 class x
10		crest 16081	. . . . . . . . . 10 class ↾t
11	7, 9, 10	co 6650	. . . . . . . . 9 class ( r ↾t x )
12		ccmp 21189	. . . . . . . . 9 class Comp
13	11, 12	wcel 1990	. . . . . . . 8 wff ( r ↾t x ) e. Comp
14	7	cuni 4436	. . . . . . . . 9 class U. r
15	14	cpw 4158	. . . . . . . 8 class ~P U. r
16	13, 8, 15	crab 2916	. . . . . . 7 class { x e. ~P U. r | ( r ↾t x ) e. Comp }
17	2	cv 1482	. . . . . . 7 class s
18		vf	. . . . . . . . . . 11 setvar f
19	18	cv 1482	. . . . . . . . . 10 class f
20	5	cv 1482	. . . . . . . . . 10 class k
21	19, 20	cima 5117	. . . . . . . . 9 class ( f " k )
22	6	cv 1482	. . . . . . . . 9 class v
23	21, 22	wss 3574	. . . . . . . 8 wff ( f " k ) C_ v
24		ccn 21028	. . . . . . . . 9 class Cn
25	7, 17, 24	co 6650	. . . . . . . 8 class ( r Cn s )
26	23, 18, 25	crab 2916	. . . . . . 7 class { f e. ( r Cn s ) | ( f " k ) C_ v }
27	5, 6, 16, 17, 26	cmpt2 6652	. . . . . 6 class ( k e. { x e. ~P U. r | ( r ↾t x ) e. Comp } , v e. s |-> { f e. ( r Cn s ) | ( f " k ) C_ v } )
28	27	crn 5115	. . . . 5 class 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 } )
29		cfi 8316	. . . . 5 class fi
30	28, 29	cfv 5888	. . . 4 class ( 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		ctg 16098	. . . 4 class topGen
32	30, 31	cfv 5888	. . 3 class ( 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	2, 3, 4, 4, 32	cmpt2 6652	. 2 class ( 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 } ) ) ) )
34	1, 33	wceq 1483	1 wff ^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 } ) ) ) )

This definition is referenced by:  xkoval  21390