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

Definition df-xko 21306
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
StepHypRef Expression
1 cxko 21304 . 2 class ^ko
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar 𝑟
4 ctop 20638 . . 3 class Top
5 vk . . . . . . 7 setvar 𝑘
6 vv . . . . . . 7 setvar 𝑣
73cv 1479 . . . . . . . . . 10 class 𝑟
8 vx . . . . . . . . . . 11 setvar 𝑥
98cv 1479 . . . . . . . . . 10 class 𝑥
10 crest 16021 . . . . . . . . . 10 class t
117, 9, 10co 6615 . . . . . . . . 9 class (𝑟t 𝑥)
12 ccmp 21129 . . . . . . . . 9 class Comp
1311, 12wcel 1987 . . . . . . . 8 wff (𝑟t 𝑥) ∈ Comp
147cuni 4409 . . . . . . . . 9 class 𝑟
1514cpw 4136 . . . . . . . 8 class 𝒫 𝑟
1613, 8, 15crab 2912 . . . . . . 7 class {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}
172cv 1479 . . . . . . 7 class 𝑠
18 vf . . . . . . . . . . 11 setvar 𝑓
1918cv 1479 . . . . . . . . . 10 class 𝑓
205cv 1479 . . . . . . . . . 10 class 𝑘
2119, 20cima 5087 . . . . . . . . 9 class (𝑓𝑘)
226cv 1479 . . . . . . . . 9 class 𝑣
2321, 22wss 3560 . . . . . . . 8 wff (𝑓𝑘) ⊆ 𝑣
24 ccn 20968 . . . . . . . . 9 class Cn
257, 17, 24co 6615 . . . . . . . 8 class (𝑟 Cn 𝑠)
2623, 18, 25crab 2912 . . . . . . 7 class {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}
275, 6, 16, 17, 26cmpt2 6617 . . . . . 6 class (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣})
2827crn 5085 . . . . 5 class ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣})
29 cfi 8276 . . . . 5 class fi
3028, 29cfv 5857 . . . 4 class (fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}))
31 ctg 16038 . . . 4 class topGen
3230, 31cfv 5857 . . 3 class (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣})))
332, 3, 4, 4, 32cmpt2 6617 . 2 class (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}))))
341, 33wceq 1480 1 wff ^ko = (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}))))
Colors of variables: wff setvar class
This definition is referenced by:  xkoval  21330
  Copyright terms: Public domain W3C validator