Theorem iskgen2

Description: A space is compactly generated iff it contains its image under the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

	Ref	Expression
Assertion	iskgen2	⊢ ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		kgentop	⊢ ( 𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top )
2		kgenidm	⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )
3		eqimss	⊢ ( ( 𝑘Gen ‘ 𝐽 ) = 𝐽 → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
4	2 3	syl	⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
5	1 4	jca	⊢ ( 𝐽 ∈ ran 𝑘Gen → ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )
6		simpr	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 )
7		kgenss	⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
8	7	adantr	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
9	6 8	eqssd	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → ( 𝑘Gen ‘ 𝐽 ) = 𝐽 )
10		kgenf	⊢ 𝑘Gen : Top ⟶ Top
11		ffn	⊢ ( 𝑘Gen : Top ⟶ Top → 𝑘Gen Fn Top )
12	10 11	ax-mp	⊢ 𝑘Gen Fn Top
13		fnfvelrn	⊢ ( ( 𝑘Gen Fn Top ∧ 𝐽 ∈ Top ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
14	12 13	mpan	⊢ ( 𝐽 ∈ Top → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
15	14	adantr	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ran 𝑘Gen )
16	9 15	eqeltrrd	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) → 𝐽 ∈ ran 𝑘Gen )
17	5 16	impbii	⊢ ( 𝐽 ∈ ran 𝑘Gen ↔ ( 𝐽 ∈ Top ∧ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝐽 ) )