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 21176
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 21174 . 2 class ^ko
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar 𝑟
4 ctop 20517 . . 3 class Top
5 vk . . . . . . 7 setvar 𝑘
6 vv . . . . . . 7 setvar 𝑣
73cv 1474 . . . . . . . . . 10 class 𝑟
8 vx . . . . . . . . . . 11 setvar 𝑥
98cv 1474 . . . . . . . . . 10 class 𝑥
10 crest 15904 . . . . . . . . . 10 class t
117, 9, 10co 6549 . . . . . . . . 9 class (𝑟t 𝑥)
12 ccmp 20999 . . . . . . . . 9 class Comp
1311, 12wcel 1977 . . . . . . . 8 wff (𝑟t 𝑥) ∈ Comp
147cuni 4372 . . . . . . . . 9 class 𝑟
1514cpw 4108 . . . . . . . 8 class 𝒫 𝑟
1613, 8, 15crab 2900 . . . . . . 7 class {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}
172cv 1474 . . . . . . 7 class 𝑠
18 vf . . . . . . . . . . 11 setvar 𝑓
1918cv 1474 . . . . . . . . . 10 class 𝑓
205cv 1474 . . . . . . . . . 10 class 𝑘
2119, 20cima 5041 . . . . . . . . 9 class (𝑓𝑘)
226cv 1474 . . . . . . . . 9 class 𝑣
2321, 22wss 3540 . . . . . . . 8 wff (𝑓𝑘) ⊆ 𝑣
24 ccn 20838 . . . . . . . . 9 class Cn
257, 17, 24co 6549 . . . . . . . 8 class (𝑟 Cn 𝑠)
2623, 18, 25crab 2900 . . . . . . 7 class {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}
275, 6, 16, 17, 26cmpt2 6551 . . . . . 6 class (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣})
2827crn 5039 . . . . 5 class ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣})
29 cfi 8199 . . . . 5 class fi
3028, 29cfv 5804 . . . 4 class (fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}))
31 ctg 15921 . . . 4 class topGen
3230, 31cfv 5804 . . 3 class (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣})))
332, 3, 4, 4, 32cmpt2 6551 . 2 class (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}))))
341, 33wceq 1475 1 wff ^ko = (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝑟 ∣ (𝑟t 𝑥) ∈ Comp}, 𝑣𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓𝑘) ⊆ 𝑣}))))
Colors of variables: wff setvar class
This definition is referenced by:  xkoval  21200
  Copyright terms: Public domain W3C validator