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