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 e. RR -> { A } e. ( Clsd ` ( topGen ` ran (,) ) ) )

Proof

Step Hyp Ref Expression
1 rehaus 
 |-  ( topGen ` ran (,) ) e. Haus
2 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
3 2 sncld 
 |-  ( ( ( topGen ` ran (,) ) e. Haus /\ A e. RR ) -> { A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
4 1 3 mpan 
 |-  ( A e. RR -> { A } e. ( Clsd ` ( topGen ` ran (,) ) ) )