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 e. ran kGen -> J e. Top )

Proof

Step	Hyp	Ref	Expression
1		kgenf	|- kGen : Top --> Top
2		frn	|- ( kGen : Top --> Top -> ran kGen C_ Top )
3	1 2	ax-mp	|- ran kGen C_ Top
4	3	sseli	|- ( J e. ran kGen -> J e. Top )