unicld

Description: A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	unicld	$⊢ (J \in Top \land A \in Fin \land A \subseteq Clsd (J)) \to ⋃ A \in Clsd (J)$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		uniiun	$⊢ ⋃ A = ⋃_{x \in A} x$
3		dfss3	$⊢ A \subseteq Clsd (J) \leftrightarrow \forall x \in A x \in Clsd (J)$
4	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)$
5	3 4	syl3an3b	$⊢ (J \in Top \land A \in Fin \land A \subseteq Clsd (J)) \to ⋃_{x \in A} x \in Clsd (J)$
6	2 5	eqeltrid	$⊢ (J \in Top \land A \in Fin \land A \subseteq Clsd (J)) \to ⋃ A \in Clsd (J)$

Metamath Proof Explorer