intcld

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

		Ref	Expression
	Assertion	intcld	$⊢ (A \neq \emptyset \land A \subseteq Clsd (J)) \to ⋂ A \in Clsd (J)$

Step	Hyp	Ref	Expression
1		intiin	$⊢ ⋂ A = ⋂_{x \in A} x$
2		dfss3	$⊢ A \subseteq Clsd (J) \leftrightarrow \forall x \in A x \in Clsd (J)$
3		iincld	$⊢ (A \neq \emptyset \land \forall x \in A x \in Clsd (J)) \to ⋂_{x \in A} x \in Clsd (J)$
4	2 3	sylan2b	$⊢ (A \neq \emptyset \land A \subseteq Clsd (J)) \to ⋂_{x \in A} x \in Clsd (J)$
5	1 4	eqeltrid	$⊢ (A \neq \emptyset \land A \subseteq Clsd (J)) \to ⋂ A \in Clsd (J)$

Metamath Proof Explorer