Metamath Proof Explorer

Theorem t1ficld

Description: In a T_1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis ist0.1 ⊢ X = ⋃ J
Assertion t1ficld ⊢ J ∈ Fre ∧ A ⊆ X ∧ A ∈ Fin → A ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 iunid ⊢ ⋃ x ∈ A x = A
3 1 ist1 ⊢ J ∈ Fre ↔ J ∈ Top ∧ ∀ x ∈ X x ∈ Clsd ⁡ J
4 3 simplbi ⊢ J ∈ Fre → J ∈ Top
5 4 3ad2ant1 ⊢ J ∈ Fre ∧ A ⊆ X ∧ A ∈ Fin → J ∈ Top
6 simp3 ⊢ J ∈ Fre ∧ A ⊆ X ∧ A ∈ Fin → A ∈ Fin
7 3 simprbi ⊢ J ∈ Fre → ∀ x ∈ X x ∈ Clsd ⁡ J
8 ssralv ⊢ A ⊆ X → ∀ x ∈ X x ∈ Clsd ⁡ J → ∀ x ∈ A x ∈ Clsd ⁡ J
9 7 8 mpan9 ⊢ J ∈ Fre ∧ A ⊆ X → ∀ x ∈ A x ∈ Clsd ⁡ J
10 9 3adant3 ⊢ J ∈ Fre ∧ A ⊆ X ∧ A ∈ Fin → ∀ x ∈ A x ∈ Clsd ⁡ J
11 1 iuncld ⊢ J ∈ Top ∧ A ∈ Fin ∧ ∀ x ∈ A x ∈ Clsd ⁡ J → ⋃ x ∈ A x ∈ Clsd ⁡ J
12 5 6 10 11 syl3anc ⊢ J ∈ Fre ∧ A ⊆ X ∧ A ∈ Fin → ⋃ x ∈ A x ∈ Clsd ⁡ J
13 2 12 eqeltrrid ⊢ J ∈ Fre ∧ A ⊆ X ∧ A ∈ Fin → A ∈ Clsd ⁡ J