Definition df-xko 23066

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 23064	. 2 class ↑ko
2		vs	. . 3 setvar 𝑠
3		vr	. . 3 setvar 𝑟
4		ctop 22394	. . 3 class Top
5		vk	. . . . . . 7 setvar 𝑘
6		vv	. . . . . . 7 setvar 𝑣
7	3	cv 1540	. . . . . . . . . 10 class 𝑟
8		vx	. . . . . . . . . . 11 setvar 𝑥
9	8	cv 1540	. . . . . . . . . 10 class 𝑥
10		crest 17365	. . . . . . . . . 10 class ↾t
11	7, 9, 10	co 7408	. . . . . . . . 9 class (𝑟 ↾t 𝑥)
12		ccmp 22889	. . . . . . . . 9 class Comp
13	11, 12	wcel 2106	. . . . . . . 8 wff (𝑟 ↾t 𝑥) ∈ Comp
14	7	cuni 4908	. . . . . . . . 9 class ∪ 𝑟
15	14	cpw 4602	. . . . . . . 8 class 𝒫 ∪ 𝑟
16	13, 8, 15	crab 3432	. . . . . . 7 class {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}
17	2	cv 1540	. . . . . . 7 class 𝑠
18		vf	. . . . . . . . . . 11 setvar 𝑓
19	18	cv 1540	. . . . . . . . . 10 class 𝑓
20	5	cv 1540	. . . . . . . . . 10 class 𝑘
21	19, 20	cima 5679	. . . . . . . . 9 class (𝑓 “ 𝑘)
22	6	cv 1540	. . . . . . . . 9 class 𝑣
23	21, 22	wss 3948	. . . . . . . 8 wff (𝑓 “ 𝑘) ⊆ 𝑣
24		ccn 22727	. . . . . . . . 9 class Cn
25	7, 17, 24	co 7408	. . . . . . . 8 class (𝑟 Cn 𝑠)
26	23, 18, 25	crab 3432	. . . . . . 7 class {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}
27	5, 6, 16, 17, 26	cmpo 7410	. . . . . 6 class (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
28	27	crn 5677	. . . . 5 class ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})
29		cfi 9404	. . . . 5 class fi
30	28, 29	cfv 6543	. . . 4 class (fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))
31		ctg 17382	. . . 4 class topGen
32	30, 31	cfv 6543	. . 3 class (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))
33	2, 3, 4, 4, 32	cmpo 7410	. 2 class (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))
34	1, 33	wceq 1541	1 wff ↑ko = (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))))

This definition is referenced by:  xkoval  23090