Metamath Proof Explorer

Definition df-xko

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)

Ref Expression
Assertion df-xko ⊢^ko=s∈Top,r∈Top⟼topGen⁡fi⁡ran⁡k∈x∈𝒫⋃r|r↾𝑡x∈Comp,v∈s⟼f∈rCns|fk⊆v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxko class^ko
1 vs setvars
2 ctop classTop
3 vr setvarr
4 ctg classtopGen
5 cfi classfi
6 vk setvark
7 vx setvarx
8 3 cv setvarr
9 8 cuni class⋃r
10 9 cpw class𝒫⋃r
11 crest class↾𝑡
12 7 cv setvarx
13 8 12 11 co classr↾𝑡x
14 ccmp classComp
15 13 14 wcel wffr↾𝑡x∈Comp
16 15 7 10 crab classx∈𝒫⋃r|r↾𝑡x∈Comp
17 vv setvarv
18 1 cv setvars
19 vf setvarf
20 ccn classCn
21 8 18 20 co classrCns
22 19 cv setvarf
23 6 cv setvark
24 22 23 cima classfk
25 17 cv setvarv
26 24 25 wss wfffk⊆v
27 26 19 21 crab classf∈rCns|fk⊆v
28 6 17 16 18 27 cmpo classk∈x∈𝒫⋃r|r↾𝑡x∈Comp,v∈s⟼f∈rCns|fk⊆v
29 28 crn classran⁡k∈x∈𝒫⋃r|r↾𝑡x∈Comp,v∈s⟼f∈rCns|fk⊆v
30 29 5 cfv classfi⁡ran⁡k∈x∈𝒫⋃r|r↾𝑡x∈Comp,v∈s⟼f∈rCns|fk⊆v
31 30 4 cfv classtopGen⁡fi⁡ran⁡k∈x∈𝒫⋃r|r↾𝑡x∈Comp,v∈s⟼f∈rCns|fk⊆v
32 1 3 2 2 31 cmpo classs∈Top,r∈Top⟼topGen⁡fi⁡ran⁡k∈x∈𝒫⋃r|r↾𝑡x∈Comp,v∈s⟼f∈rCns|fk⊆v
33 0 32 wceq wff^ko=s∈Top,r∈Top⟼topGen⁡fi⁡ran⁡k∈x∈𝒫⋃r|r↾𝑡x∈Comp,v∈s⟼f∈rCns|fk⊆v