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

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