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 ` (/) )