Theorem unicld

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

	Ref	Expression
Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	unicld	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ) → ∪ 𝐴 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
3		dfss3	⊢ ( 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
4	1	iuncld	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ∪ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
5	3 4	syl3an3b	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ) → ∪ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
6	2 5	eqeltrid	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ) → ∪ 𝐴 ∈ ( Clsd ‘ 𝐽 ) )