# Metamath Proof Explorer

## 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
`|- ( J e. ran kGen <-> ( J e. Top /\ ( kGen ` J ) C_ J ) )`

### Proof

Step Hyp Ref Expression
1 kgentop
` |-  ( J e. ran kGen -> J e. Top )`
2 kgenidm
` |-  ( J e. ran kGen -> ( kGen ` J ) = J )`
3 eqimss
` |-  ( ( kGen ` J ) = J -> ( kGen ` J ) C_ J )`
4 2 3 syl
` |-  ( J e. ran kGen -> ( kGen ` J ) C_ J )`
5 1 4 jca
` |-  ( J e. ran kGen -> ( J e. Top /\ ( kGen ` J ) C_ J ) )`
6 simpr
` |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) -> ( kGen ` J ) C_ J )`
7 kgenss
` |-  ( J e. Top -> J C_ ( kGen ` J ) )`
` |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) -> J C_ ( kGen ` J ) )`
9 6 8 eqssd
` |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) -> ( kGen ` J ) = J )`
10 kgenf
` |-  kGen : Top --> Top`
11 ffn
` |-  ( kGen : Top --> Top -> kGen Fn Top )`
12 10 11 ax-mp
` |-  kGen Fn Top`
13 fnfvelrn
` |-  ( ( kGen Fn Top /\ J e. Top ) -> ( kGen ` J ) e. ran kGen )`
14 12 13 mpan
` |-  ( J e. Top -> ( kGen ` J ) e. ran kGen )`
` |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) -> ( kGen ` J ) e. ran kGen )`
` |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) -> J e. ran kGen )`
` |-  ( J e. ran kGen <-> ( J e. Top /\ ( kGen ` J ) C_ J ) )`