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 ) )
8 7 adantr 
 |-  ( ( 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 )
15 14 adantr 
 |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) -> ( kGen ` J ) e. ran kGen )
16 9 15 eqeltrrd 
 |-  ( ( J e. Top /\ ( kGen ` J ) C_ J ) -> J e. ran kGen )
17 5 16 impbii 
 |-  ( J e. ran kGen <-> ( J e. Top /\ ( kGen ` J ) C_ J ) )