Definition df-xko 23937

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

Distinct variable group:   𝑓,𝑘,𝑟,𝑠,𝑣,𝑥

Detailed syntax breakdown of Definition df-xko

Step	Hyp	Ref	Expression
1		cxko 23935	. 2 class ↑ko
2		vs	. . 3 setvar 𝑠
3		vr	. . 3 setvar 𝑟
4		ctop 23266	. . 3 class Top
5		vk	. . . . . . 7 setvar 𝑘
6		vv	. . . . . . 7 setvar 𝑣
7	3	cv 1569	. . . . . . . . . 10 class 𝑟
8		vx	. . . . . . . . . . 11 setvar 𝑥
9	8	cv 1569	. . . . . . . . . 10 class 𝑥
10		crest 17641	. . . . . . . . . 10 class ↾t
11	7, 9, 10	co 7451	. . . . . . . . 9 class (𝑟 ↾t 𝑥)
12		ccmp 23759	. . . . . . . . 9 class Comp
13	11, 12	wcel 2147	. . . . . . . 8 wff (𝑟 ↾t 𝑥) ∈ Comp
14	7	cuni 4872	. . . . . . . . 9 class ∪ 𝑟
15	14	cpw 4560	. . . . . . . 8 class 𝒫 ∪ 𝑟
16	13, 8, 15	crab 3416	. . . . . . 7 class {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}
17	2	cv 1569	. . . . . . 7 class 𝑠
18		vf	. . . . . . . . . . 11 setvar 𝑓
19	18	cv 1569	. . . . . . . . . 10 class 𝑓
20	5	cv 1569	. . . . . . . . . 10 class 𝑘
21	19, 20	cima 5661	. . . . . . . . 9 class (𝑓 “ 𝑘)
22	6	cv 1569	. . . . . . . . 9 class 𝑣
23	21, 22	wss 3900	. . . . . . . 8 wff (𝑓 “ 𝑘) ⊆ 𝑣
24		ccn 23597	. . . . . . . . 9 class Cn
25	7, 17, 24	co 7451	. . . . . . . 8 class (𝑟 Cn 𝑠)
26	23, 18, 25	crab 3416	. . . . . . 7 class {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}
27	5, 6, 16, 17, 26	cmpo 7453	. . . . . 6 class (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
28	27	crn 5659	. . . . 5 class ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
29		cfi 9439	. . . . 5 class fi
30	28, 29	cfv 6566	. . . 4 class (fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
31		ctg 17658	. . . 4 class topGen
32	30, 31	cfv 6566	. . 3 class (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))
33	2, 3, 4, 4, 32	cmpo 7453	. 2 class (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
34	1, 33	wceq 1570	1 wff ↑ko = (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))

This definition is used by:  xkoval  23961