Theorem disllycmp

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

	Ref	Expression
Assertion	disllycmp	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally Comp )

Proof

Step	Hyp	Ref	Expression
1		snfi	⊢ { 𝑥 } ∈ Fin
2		discmp	⊢ ( { 𝑥 } ∈ Fin ↔ 𝒫 { 𝑥 } ∈ Comp )
3	1 2	mpbi	⊢ 𝒫 { 𝑥 } ∈ Comp
4	3	rgenw	⊢ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ Comp
5		dislly	⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 ∈ Locally Comp ↔ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ Comp ) )
6	4 5	mpbiri	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally Comp )