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 \in Fre \land A \subseteq X \land A \in Fin) \to A \in Clsd (J)$

Step	Hyp	Ref	Expression
1		ist0.1	$⊢ X = ⋃ J$
2		iunid	$⊢ ⋃_{x \in A} \{x\} = A$
3	1	ist1	$⊢ J \in Fre \leftrightarrow (J \in Top \land \forall x \in X \{x\} \in Clsd (J))$
4	3	simplbi	$⊢ J \in Fre \to J \in Top$
5	4	3ad2ant1	$⊢ (J \in Fre \land A \subseteq X \land A \in Fin) \to J \in Top$
6		simp3	$⊢ (J \in Fre \land A \subseteq X \land A \in Fin) \to A \in Fin$
7	3	simprbi	$⊢ J \in Fre \to \forall x \in X \{x\} \in Clsd (J)$
8		ssralv	$⊢ A \subseteq X \to (\forall x \in X \{x\} \in Clsd (J) \to \forall x \in A \{x\} \in Clsd (J))$
9	7 8	mpan9	$⊢ (J \in Fre \land A \subseteq X) \to \forall x \in A \{x\} \in Clsd (J)$
10	9	3adant3	$⊢ (J \in Fre \land A \subseteq X \land A \in Fin) \to \forall x \in A \{x\} \in Clsd (J)$
11	1	iuncld	$⊢ (J \in Top \land A \in Fin \land \forall x \in A \{x\} \in Clsd (J)) \to ⋃_{x \in A} \{x\} \in Clsd (J)$
12	5 6 10 11	syl3anc	$⊢ (J \in Fre \land A \subseteq X \land A \in Fin) \to ⋃_{x \in A} \{x\} \in Clsd (J)$
13	2 12	eqeltrrid	$⊢ (J \in Fre \land A \subseteq X \land A \in Fin) \to A \in Clsd (J)$

Metamath Proof Explorer