Theorem sn0topon

Description: The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	sn0topon	⊢ { ∅ } ∈ ( TopOn ‘ ∅ )

Proof

Step	Hyp	Ref	Expression
1		pw0	⊢ 𝒫 ∅ = { ∅ }
2		0ex	⊢ ∅ ∈ V
3		distopon	⊢ ( ∅ ∈ V → 𝒫 ∅ ∈ ( TopOn ‘ ∅ ) )
4	2 3	ax-mp	⊢ 𝒫 ∅ ∈ ( TopOn ‘ ∅ )
5	1 4	eqeltrri	⊢ { ∅ } ∈ ( TopOn ‘ ∅ )