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 )