Theorem sncld

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	⊢ 𝑋 = ∪ 𝐽
Assertion	sncld	⊢ ( ( 𝐽 ∈ Haus ∧ 𝑃 ∈ 𝑋 ) → { 𝑃 } ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	⊢ 𝑋 = ∪ 𝐽
2		haust1	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Fre )
3	1	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ 𝑃 ∈ 𝑋 ) → { 𝑃 } ∈ ( Clsd ‘ 𝐽 ) )
4	2 3	sylan	⊢ ( ( 𝐽 ∈ Haus ∧ 𝑃 ∈ 𝑋 ) → { 𝑃 } ∈ ( Clsd ‘ 𝐽 ) )