Description: A singleton is closed in a Hausdorff space. (Contributed by NM, 5-Mar-2007) (Revised by Mario Carneiro, 24-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | t1sep.1 | |- X = U. J |
|
Assertion | sncld | |- ( ( J e. Haus /\ P e. X ) -> { P } e. ( Clsd ` J ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | t1sep.1 | |- X = U. J |
|
2 | haust1 | |- ( J e. Haus -> J e. Fre ) |
|
3 | 1 | t1sncld | |- ( ( J e. Fre /\ P e. X ) -> { P } e. ( Clsd ` J ) ) |
4 | 2 3 | sylan | |- ( ( J e. Haus /\ P e. X ) -> { P } e. ( Clsd ` J ) ) |