Theorem kgentop

Description: A compactly generated space is a topology. (Note: henceforth we will use the idiom " J e. ran kGen " to denote " J is compactly generated", since as we will show a space is compactly generated iff it is in the range of the compact generator.) (Contributed by Mario Carneiro, 20-Mar-2015)

	Ref	Expression
Assertion	kgentop	$$⊢J\in \mathrm{ran}\mathrm{𝑘Gen}\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		kgenf	$$⊢\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}$$
2		frn	$$⊢\mathrm{𝑘Gen}:\mathrm{Top}⟶\mathrm{Top}\to \mathrm{ran}\mathrm{𝑘Gen}\subseteq \mathrm{Top}$$
3	1 2	ax-mp	$$⊢\mathrm{ran}\mathrm{𝑘Gen}\subseteq \mathrm{Top}$$
4	3	sseli	$$⊢J\in \mathrm{ran}\mathrm{𝑘Gen}\to J\in \mathrm{Top}$$