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	⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		kgenf	⊢ 𝑘Gen : Top ⟶ Top
2		frn	⊢ ( 𝑘Gen : Top ⟶ Top → ran 𝑘Gen ⊆ Top )
3	1 2	ax-mp	⊢ ran 𝑘Gen ⊆ Top
4	3	sseli	⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )