Metamath Proof Explorer

Theorem disllycmp

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

Ref Expression
Assertion disllycmp ⊢ X ∈ V → 𝒫 X ∈ Locally Comp

Proof

Step Hyp Ref Expression
1 snfi ⊢ x ∈ Fin
2 discmp ⊢ x ∈ Fin ↔ 𝒫 x ∈ Comp
3 1 2 mpbi ⊢ 𝒫 x ∈ Comp
4 3 rgenw ⊢ ∀ x ∈ X 𝒫 x ∈ Comp
5 dislly ⊢ X ∈ V → 𝒫 X ∈ Locally Comp ↔ ∀ x ∈ X 𝒫 x ∈ Comp
6 4 5 mpbiri ⊢ X ∈ V → 𝒫 X ∈ Locally Comp