This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑠 ∈ Top , 𝑟 ∈ Top ↦ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxko ⊢ ↑ko
1 vs ⊢ 𝑠
2 ctop ⊢ Top
3 vr ⊢ 𝑟
4 ctg ⊢ topGen
5 cfi ⊢ fi
6 vk ⊢ 𝑘
7 vx ⊢ 𝑥
8 3 cv ⊢ 𝑟
9 8 cuni ⊢ ∪ 𝑟
10 9 cpw ⊢ 𝒫 ∪ 𝑟
11 crest ⊢ ↾t
12 7 cv ⊢ 𝑥
13 8 12 11 co ⊢ ( 𝑟 ↾t 𝑥 )
14 ccmp ⊢ Comp
15 13 14 wcel ⊢ ( 𝑟 ↾t 𝑥 ) ∈ Comp
16 15 7 10 crab ⊢ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp }
17 vv ⊢ 𝑣
18 1 cv ⊢ 𝑠
19 vf ⊢ 𝑓
20 ccn ⊢ Cn
21 8 18 20 co ⊢ ( 𝑟 Cn 𝑠 )
22 19 cv ⊢ 𝑓
23 6 cv ⊢ 𝑘
24 22 23 cima ⊢ ( 𝑓 “ 𝑘 )
25 17 cv ⊢ 𝑣
26 24 25 wss ⊢ ( 𝑓 “ 𝑘 ) ⊆ 𝑣
27 26 19 21 crab ⊢ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 }
28 6 17 16 18 27 cmpo ⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
29 28 crn ⊢ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } )
30 29 5 cfv ⊢ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) )
31 30 4 cfv ⊢ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) )
32 1 3 2 2 31 cmpo ⊢ ( 𝑠 ∈ Top , 𝑟 ∈ Top ↦ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )
33 0 32 wceq ⊢ ↑ko = ( 𝑠 ∈ Top , 𝑟 ∈ Top ↦ ( topGen ‘ ( fi ‘ ran ( 𝑘 ∈ { 𝑥 ∈ 𝒫 ∪ 𝑟 ∣ ( 𝑟 ↾t 𝑥 ) ∈ Comp } , 𝑣 ∈ 𝑠 ↦ { 𝑓 ∈ ( 𝑟 Cn 𝑠 ) ∣ ( 𝑓 “ 𝑘 ) ⊆ 𝑣 } ) ) ) )