Metamath Proof Explorer

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 
|- { (/) } e. ( TopOn ` (/) )

Proof

Step Hyp Ref Expression
1 pw0 
 |-  ~P (/) = { (/) }
2 0ex 
 |-  (/) e. _V
3 distopon 
 |-  ( (/) e. _V -> ~P (/) e. ( TopOn ` (/) ) )
4 2 3 ax-mp 
 |-  ~P (/) e. ( TopOn ` (/) )
5 1 4 eqeltrri 
 |-  { (/) } e. ( TopOn ` (/) )