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 𝑋 = 𝐽
Assertion t1ficld ( ( 𝐽 ∈ Fre ∧ 𝐴𝑋𝐴 ∈ Fin ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 ist0.1 𝑋 = 𝐽
2 iunid 𝑥𝐴 { 𝑥 } = 𝐴
3 1 ist1 ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) )
4 3 simplbi ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
5 4 3ad2ant1 ( ( 𝐽 ∈ Fre ∧ 𝐴𝑋𝐴 ∈ Fin ) → 𝐽 ∈ Top )
6 simp3 ( ( 𝐽 ∈ Fre ∧ 𝐴𝑋𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
7 3 simprbi ( 𝐽 ∈ Fre → ∀ 𝑥𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
8 ssralv ( 𝐴𝑋 → ( ∀ 𝑥𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) → ∀ 𝑥𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) )
9 7 8 mpan9 ( ( 𝐽 ∈ Fre ∧ 𝐴𝑋 ) → ∀ 𝑥𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
10 9 3adant3 ( ( 𝐽 ∈ Fre ∧ 𝐴𝑋𝐴 ∈ Fin ) → ∀ 𝑥𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
11 1 iuncld ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
12 5 6 10 11 syl3anc ( ( 𝐽 ∈ Fre ∧ 𝐴𝑋𝐴 ∈ Fin ) → 𝑥𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
13 2 12 eqeltrrid ( ( 𝐽 ∈ Fre ∧ 𝐴𝑋𝐴 ∈ Fin ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )