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 22820
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 22818 . 2 class ↑ko
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar π‘Ÿ
4 ctop 22148 . . 3 class Top
5 vk . . . . . . 7 setvar π‘˜
6 vv . . . . . . 7 setvar 𝑣
73cv 1539 . . . . . . . . . 10 class π‘Ÿ
8 vx . . . . . . . . . . 11 setvar π‘₯
98cv 1539 . . . . . . . . . 10 class π‘₯
10 crest 17228 . . . . . . . . . 10 class β†Ύt
117, 9, 10co 7337 . . . . . . . . 9 class (π‘Ÿ β†Ύt π‘₯)
12 ccmp 22643 . . . . . . . . 9 class Comp
1311, 12wcel 2105 . . . . . . . 8 wff (π‘Ÿ β†Ύt π‘₯) ∈ Comp
147cuni 4852 . . . . . . . . 9 class βˆͺ π‘Ÿ
1514cpw 4547 . . . . . . . 8 class 𝒫 βˆͺ π‘Ÿ
1613, 8, 15crab 3403 . . . . . . 7 class {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}
172cv 1539 . . . . . . 7 class 𝑠
18 vf . . . . . . . . . . 11 setvar 𝑓
1918cv 1539 . . . . . . . . . 10 class 𝑓
205cv 1539 . . . . . . . . . 10 class π‘˜
2119, 20cima 5623 . . . . . . . . 9 class (𝑓 β€œ π‘˜)
226cv 1539 . . . . . . . . 9 class 𝑣
2321, 22wss 3898 . . . . . . . 8 wff (𝑓 β€œ π‘˜) βŠ† 𝑣
24 ccn 22481 . . . . . . . . 9 class Cn
257, 17, 24co 7337 . . . . . . . 8 class (π‘Ÿ Cn 𝑠)
2623, 18, 25crab 3403 . . . . . . 7 class {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}
275, 6, 16, 17, 26cmpo 7339 . . . . . 6 class (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣})
2827crn 5621 . . . . 5 class ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣})
29 cfi 9267 . . . . 5 class fi
3028, 29cfv 6479 . . . 4 class (fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}))
31 ctg 17245 . . . 4 class topGen
3230, 31cfv 6479 . . 3 class (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣})))
332, 3, 4, 4, 32cmpo 7339 . 2 class (𝑠 ∈ Top, π‘Ÿ ∈ Top ↦ (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}))))
341, 33wceq 1540 1 wff ↑ko = (𝑠 ∈ Top, π‘Ÿ ∈ Top ↦ (topGenβ€˜(fiβ€˜ran (π‘˜ ∈ {π‘₯ ∈ 𝒫 βˆͺ π‘Ÿ ∣ (π‘Ÿ β†Ύt π‘₯) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (π‘Ÿ Cn 𝑠) ∣ (𝑓 β€œ π‘˜) βŠ† 𝑣}))))
Colors of variables: wff setvar class
This definition is referenced by:  xkoval  22844
  Copyright terms: Public domain W3C validator