Theorem unicld

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

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	unicld	|- ( ( J e. Top /\ A e. Fin /\ A C_ ( Clsd ` J ) ) -> U. A e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		uniiun	|- U. A = U_ x e. A x
3		dfss3	|- ( A C_ ( Clsd ` J ) <-> A. x e. A x e. ( Clsd ` J ) )
4	1	iuncld	|- ( ( J e. Top /\ A e. Fin /\ A. x e. A x e. ( Clsd ` J ) ) -> U_ x e. A x e. ( Clsd ` J ) )
5	3 4	syl3an3b	|- ( ( J e. Top /\ A e. Fin /\ A C_ ( Clsd ` J ) ) -> U_ x e. A x e. ( Clsd ` J ) )
6	2 5	eqeltrid	|- ( ( J e. Top /\ A e. Fin /\ A C_ ( Clsd ` J ) ) -> U. A e. ( Clsd ` J ) )