Theorem intcld

Description: The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006)

	Ref	Expression
Assertion	intcld	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ) → ∩ 𝐴 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
2		dfss3	⊢ ( 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
3		iincld	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
4	2 3	sylan2b	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ 𝐴 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
5	1 4	eqeltrid	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ( Clsd ‘ 𝐽 ) ) → ∩ 𝐴 ∈ ( Clsd ‘ 𝐽 ) )