Metamath Proof Explorer
Description: The singleton of the empty set is a topology. (Contributed by Stefan
Allan, 3Mar2006) (Proof shortened by Mario Carneiro, 13Aug2015)


Ref 
Expression 

Assertion 
sn0top 
$${\u22a2}\left\{\varnothing \right\}\in \mathrm{Top}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

sn0topon 
$${\u22a2}\left\{\varnothing \right\}\in \mathrm{TopOn}\left(\varnothing \right)$$ 
2 
1

topontopi 
$${\u22a2}\left\{\varnothing \right\}\in \mathrm{Top}$$ 