Metamath Proof Explorer


Theorem sncldre

Description: A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion sncldre A A Clsd topGen ran .

Proof

Step Hyp Ref Expression
1 rehaus topGen ran . Haus
2 uniretop = topGen ran .
3 2 sncld topGen ran . Haus A A Clsd topGen ran .
4 1 3 mpan A A Clsd topGen ran .