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