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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kgentop | |
|
2 | kgenidm | |
|
3 | eqimss | |
|
4 | 2 3 | syl | |
5 | 1 4 | jca | |
6 | simpr | |
|
7 | kgenss | |
|
8 | 7 | adantr | |
9 | 6 8 | eqssd | |
10 | kgenf | |
|
11 | ffn | |
|
12 | 10 11 | ax-mp | |
13 | fnfvelrn | |
|
14 | 12 13 | mpan | |
15 | 14 | adantr | |
16 | 9 15 | eqeltrrd | |
17 | 5 16 | impbii | |