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 ∈ r Cn s | f k ⊆ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxko class ^ ko
1 vs setvar s
2 ctop class Top
3 vr setvar r
4 ctg class topGen
5 cfi class fi
6 vk setvar k
7 vx setvar x
8 3 cv setvar r
9 8 cuni class ⋃ r
10 9 cpw class 𝒫 ⋃ r
11 crest class ↾ 𝑡
12 7 cv setvar x
13 8 12 11 co class r ↾ 𝑡 x
14 ccmp class Comp
15 13 14 wcel wff r ↾ 𝑡 x ∈ Comp
16 15 7 10 crab class x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp
17 vv setvar v
18 1 cv setvar s
19 vf setvar f
20 ccn class Cn
21 8 18 20 co class r Cn s
22 19 cv setvar f
23 6 cv setvar k
24 22 23 cima class f k
25 17 cv setvar v
26 24 25 wss wff f k ⊆ v
27 26 19 21 crab class f ∈ r Cn s | f k ⊆ v
28 6 17 16 18 27 cmpo class k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v
29 28 crn class ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v
30 29 5 cfv class fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v
31 30 4 cfv class topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v
32 1 3 2 2 31 cmpo class s ∈ Top , r ∈ Top ⟼ topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v
33 0 32 wceq wff ^ ko = s ∈ Top , r ∈ Top ⟼ topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ r | r ↾ 𝑡 x ∈ Comp , v ∈ s ⟼ f ∈ r Cn s | f k ⊆ v