Metamath Proof Explorer


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 ‘ 𝐽 ) )