This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ X = ⋃ J
Assertion t1sncld ⊢ J ∈ Fre ∧ A ∈ X → A ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 1 ist1 ⊢ J ∈ Fre ↔ J ∈ Top ∧ ∀ x ∈ X x ∈ Clsd ⁡ J
3 sneq ⊢ x = A → x = A
4 3 eleq1d ⊢ x = A → x ∈ Clsd ⁡ J ↔ A ∈ Clsd ⁡ J
5 4 rspccv ⊢ ∀ x ∈ X x ∈ Clsd ⁡ J → A ∈ X → A ∈ Clsd ⁡ J
6 2 5 simplbiim ⊢ J ∈ Fre → A ∈ X → A ∈ Clsd ⁡ J
7 6 imp ⊢ J ∈ Fre ∧ A ∈ X → A ∈ Clsd ⁡ J