Metamath Proof Explorer

Theorem llycmpkgen

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

Ref Expression
Assertion llycmpkgen 
|- ( J e. N-Locally Comp -> J e. ran kGen )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 nllytop 
 |-  ( J e. N-Locally Comp -> J e. Top )
3 simpl 
 |-  ( ( J e. N-Locally Comp /\ x e. U. J ) -> J e. N-Locally Comp )
4 1 topopn 
 |-  ( J e. Top -> U. J e. J )
5 2 4 syl 
 |-  ( J e. N-Locally Comp -> U. J e. J )
6 5 adantr 
 |-  ( ( J e. N-Locally Comp /\ x e. U. J ) -> U. J e. J )
7 simpr 
 |-  ( ( J e. N-Locally Comp /\ x e. U. J ) -> x e. U. J )
8 nllyi 
 |-  ( ( J e. N-Locally Comp /\ U. J e. J /\ x e. U. J ) -> E. k e. ( ( nei ` J ) ` { x } ) ( k C_ U. J /\ ( J |`t k ) e. Comp ) )
9 3 6 7 8 syl3anc 
 |-  ( ( J e. N-Locally Comp /\ x e. U. J ) -> E. k e. ( ( nei ` J ) ` { x } ) ( k C_ U. J /\ ( J |`t k ) e. Comp ) )
10 simpr 
 |-  ( ( k C_ U. J /\ ( J |`t k ) e. Comp ) -> ( J |`t k ) e. Comp )
11 10 reximi 
 |-  ( E. k e. ( ( nei ` J ) ` { x } ) ( k C_ U. J /\ ( J |`t k ) e. Comp ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
12 9 11 syl 
 |-  ( ( J e. N-Locally Comp /\ x e. U. J ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
13 1 2 12 llycmpkgen2 
 |-  ( J e. N-Locally Comp -> J e. ran kGen )