Theorem disllycmp

Description: A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015)

	Ref	Expression
Assertion	disllycmp	|- ( X e. V -> ~P X e. Locally Comp )

Proof

Step	Hyp	Ref	Expression
1		snfi	|- { x } e. Fin
2		discmp	|- ( { x } e. Fin <-> ~P { x } e. Comp )
3	1 2	mpbi	|- ~P { x } e. Comp
4	3	rgenw	|- A. x e. X ~P { x } e. Comp
5		dislly	|- ( X e. V -> ( ~P X e. Locally Comp <-> A. x e. X ~P { x } e. Comp ) )
6	4 5	mpbiri	|- ( X e. V -> ~P X e. Locally Comp )