xkotop

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

		Ref	Expression
	Assertion	xkotop	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ R = ⋃ R$
2		eqid	$⊢ \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\} = \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}$
3		eqid	$⊢ (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
4	1 2 3	xkoval	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R = topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
5		fibas	$⊢ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \in TopBases$
6		tgcl	$⊢ fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})) \in TopBases \to topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))) \in Top$
7	5 6	ax-mp	$⊢ topGen (fi (ran (k \in \{x \in 𝒫 ⋃ R \| R ↾_{𝑡} x \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}))) \in Top$
8	4 7	eqeltrdi	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$

Metamath Proof Explorer