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 = ( 𝑠 ∈ Top , 𝑟 ∈ Top ↦ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxko	⊢ ↑ko
1		vs	⊢ 𝑠
2		ctop	⊢ Top
3		vr	⊢ 𝑟
4		ctg	⊢ topGen
5		cfi	⊢ fi
6		vk	⊢ 𝑘
7		vx	⊢ 𝑥
8	3	cv	⊢ 𝑟
9	8	cuni	⊢ ∪ 𝑟
10	9	cpw	⊢ 𝒫 ∪ 𝑟
11		crest	⊢ ↾t
12	7	cv	⊢ 𝑥
13	8 12 11	co	⊢ ( 𝑟 ↾t 𝑥 )
14		ccmp	⊢ Comp
15	13 14	wcel	⊢ ( 𝑟 ↾t 𝑥 ) ∈ Comp
16	15 7 10	crab	⊢ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp }
17		vv	⊢ 𝑣
18	1	cv	⊢ 𝑠
19		vf	⊢ 𝑓
20		ccn	⊢ Cn
21	8 18 20	co	⊢ ( 𝑟 Cn 𝑠 )
22	19	cv	⊢ 𝑓
23	6	cv	⊢ 𝑘
24	22 23	cima	⊢ ( 𝑓 “ 𝑘 )
25	17	cv	⊢ 𝑣
26	24 25	wss	⊢ ( 𝑓 “ 𝑘 ) ⊆ 𝑣
27	26 19 21	crab	⊢ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 }
28	6 17 16 18 27	cmpo	⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
29	28	crn	⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
30	29 5	cfv	⊢ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
31	30 4	cfv	⊢ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
32	1 3 2 2 31	cmpo	⊢ ( 𝑠 ∈ Top , 𝑟 ∈ Top ↦ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
33	0 32	wceq	⊢ ↑ko = ( 𝑠 ∈ Top , 𝑟 ∈ Top ↦ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )