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 23067
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 23065 . 2 class ↑ko
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar π‘Ÿ
4 ctop 22395 . . 3 class Top
5 vk . . . . . . 7 setvar π‘˜
6 vv . . . . . . 7 setvar 𝑣
73cv 1541 . . . . . . . . . 10 class π‘Ÿ
8 vx . . . . . . . . . . 11 setvar π‘₯
98cv 1541 . . . . . . . . . 10 class π‘₯
10 crest 17366 . . . . . . . . . 10 class β†Ύt
117, 9, 10co 7409 . . . . . . . . 9 class (π‘Ÿ β†Ύt π‘₯)
12 ccmp 22890 . . . . . . . . 9 class Comp
1311, 12wcel 2107 . . . . . . . 8 wff (π‘Ÿ β†Ύt π‘₯) ∈ Comp
147cuni 4909 . . . . . . . . 9 class βˆͺ π‘Ÿ
1514cpw 4603 . . . . . . . 8 class 𝒫 βˆͺ π‘Ÿ
1613, 8, 15crab 3433 . . . . . . 7 class {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}
172cv 1541 . . . . . . 7 class 𝑠
18 vf . . . . . . . . . . 11 setvar 𝑓
1918cv 1541 . . . . . . . . . 10 class 𝑓
205cv 1541 . . . . . . . . . 10 class π‘˜
2119, 20cima 5680 . . . . . . . . 9 class (𝑓 β€œ π‘˜)
226cv 1541 . . . . . . . . 9 class 𝑣
2321, 22wss 3949 . . . . . . . 8 wff (𝑓 β€œ π‘˜) βŠ† 𝑣
24 ccn 22728 . . . . . . . . 9 class Cn
257, 17, 24co 7409 . . . . . . . 8 class (π‘Ÿ Cn 𝑠)
2623, 18, 25crab 3433 . . . . . . 7 class {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}
275, 6, 16, 17, 26cmpo 7411 . . . . . 6 class (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣})
2827crn 5678 . . . . 5 class ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣})
29 cfi 9405 . . . . 5 class fi
3028, 29cfv 6544 . . . 4 class (fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}))
31 ctg 17383 . . . 4 class topGen
3230, 31cfv 6544 . . 3 class (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣})))
332, 3, 4, 4, 32cmpo 7411 . 2 class (𝑠 ∈ Top, π‘Ÿ ∈ Top ↦ (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}))))
341, 33wceq 1542 1 wff ↑ko = (𝑠 ∈ Top, π‘Ÿ ∈ Top ↦ (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}))))
Colors of variables: wff setvar class
This definition is referenced by:  xkoval  23091
  Copyright terms: Public domain W3C validator