This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmpkgen

Description: A compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion cmpkgen 
|- ( J e. Comp -> J e. ran kGen )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 cmptop 
 |-  ( J e. Comp -> J e. Top )
3 2 adantr 
 |-  ( ( J e. Comp /\ x e. U. J ) -> J e. Top )
4 1 topopn 
 |-  ( J e. Top -> U. J e. J )
5 3 4 syl 
 |-  ( ( J e. Comp /\ x e. U. J ) -> U. J e. J )
6 simpr 
 |-  ( ( J e. Comp /\ x e. U. J ) -> x e. U. J )
7 6 snssd 
 |-  ( ( J e. Comp /\ x e. U. J ) -> { x } C_ U. J )
8 opnneiss 
 |-  ( ( J e. Top /\ U. J e. J /\ { x } C_ U. J ) -> U. J e. ( ( nei ` J ) ` { x } ) )
9 3 5 7 8 syl3anc 
 |-  ( ( J e. Comp /\ x e. U. J ) -> U. J e. ( ( nei ` J ) ` { x } ) )
10 1 restid 
 |-  ( J e. Top -> ( J |`t U. J ) = J )
11 3 10 syl 
 |-  ( ( J e. Comp /\ x e. U. J ) -> ( J |`t U. J ) = J )
12 simpl 
 |-  ( ( J e. Comp /\ x e. U. J ) -> J e. Comp )
13 11 12 eqeltrd 
 |-  ( ( J e. Comp /\ x e. U. J ) -> ( J |`t U. J ) e. Comp )
14 oveq2 
 |-  ( k = U. J -> ( J |`t k ) = ( J |`t U. J ) )
15 14 eleq1d 
 |-  ( k = U. J -> ( ( J |`t k ) e. Comp <-> ( J |`t U. J ) e. Comp ) )
16 15 rspcev 
 |-  ( ( U. J e. ( ( nei ` J ) ` { x } ) /\ ( J |`t U. J ) e. Comp ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
17 9 13 16 syl2anc 
 |-  ( ( J e. Comp /\ x e. U. J ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
18 1 2 17 llycmpkgen2 
 |-  ( J e. Comp -> J e. ran kGen )