Metamath Proof Explorer

Theorem xkotop

Description: The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion xkotop ⊢ R ∈ Top ∧ S ∈ Top → S ^ ko R ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ R = ⋃ R
2 eqid ⊢ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp = x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp
3 eqid ⊢ k ∈ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v = k ∈ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v
4 1 2 3 xkoval ⊢ R ∈ Top ∧ S ∈ Top → S ^ ko R = topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v
5 fibas ⊢ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v ∈ TopBases
6 tgcl ⊢ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v ∈ TopBases → topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v ∈ Top
7 5 6 ax-mp ⊢ topGen ⁡ fi ⁡ ran ⁡ k ∈ x ∈ 𝒫 ⋃ R | R ↾ 𝑡 x ∈ Comp , v ∈ S ⟼ f ∈ R Cn S | f k ⊆ v ∈ Top
8 4 7 eqeltrdi ⊢ R ∈ Top ∧ S ∈ Top → S ^ ko R ∈ Top