disllycmp

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

		Ref	Expression
	Assertion	disllycmp	$⊢ X \in V \to 𝒫 X \in LocallyComp$

Step	Hyp	Ref	Expression
1		snfi	$⊢ \{x\} \in Fin$
2		discmp	$⊢ \{x\} \in Fin \leftrightarrow 𝒫 \{x\} \in Comp$
3	1 2	mpbi	$⊢ 𝒫 \{x\} \in Comp$
4	3	rgenw	$⊢ \forall x \in X 𝒫 \{x\} \in Comp$
5		dislly	$⊢ X \in V \to (𝒫 X \in LocallyComp\leftrightarrow\forall x \in X 𝒫 \{x\} \in Comp)$
6	4 5	mpbiri	$⊢ X \in V \to 𝒫 X \in LocallyComp$

Metamath Proof Explorer