Theorem t1sncld

Description: In a T_1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010)

	Ref	Expression
Hypothesis	ist0.1	⊢ 𝑋 = ∪ 𝐽
Assertion	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	⊢ 𝑋 = ∪ 𝐽
2	1	ist1	⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) )
3		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
4	3	eleq1d	⊢ ( 𝑥 = 𝐴 → ( { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ↔ { 𝐴 } ∈ ( Clsd ‘ 𝐽 ) ) )
5	4	rspccv	⊢ ( ∀ 𝑥 ∈ 𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) → ( 𝐴 ∈ 𝑋 → { 𝐴 } ∈ ( Clsd ‘ 𝐽 ) ) )
6	2 5	simplbiim	⊢ ( 𝐽 ∈ Fre → ( 𝐴 ∈ 𝑋 → { 𝐴 } ∈ ( Clsd ‘ 𝐽 ) ) )
7	6	imp	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ∈ ( Clsd ‘ 𝐽 ) )