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

Metamath Proof Explorer

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 )