Metamath Proof Explorer


Theorem 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 Top A Fin A Clsd J A Clsd J

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 uniiun A = x A x
3 dfss3 A Clsd J x A x Clsd J
4 1 iuncld J Top A Fin x A x Clsd J x A x Clsd J
5 3 4 syl3an3b J Top A Fin A Clsd J x A x Clsd J
6 2 5 eqeltrid J Top A Fin A Clsd J A Clsd J