clscld

Description: The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	clscld	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \in Clsd (J)$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	clsval	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
3	1	topcld	$⊢ J \in Top \to X \in Clsd (J)$
4	3	anim1i	$⊢ (J \in Top \land S \subseteq X) \to (X \in Clsd (J) \land S \subseteq X)$
5		sseq2	$⊢ x = X \to (S \subseteq x \leftrightarrow S \subseteq X)$
6	5	elrab	$⊢ X \in \{x \in Clsd (J) \| S \subseteq x\} \leftrightarrow (X \in Clsd (J) \land S \subseteq X)$
7	4 6	sylibr	$⊢ (J \in Top \land S \subseteq X) \to X \in \{x \in Clsd (J) \| S \subseteq x\}$
8	7	ne0d	$⊢ (J \in Top \land S \subseteq X) \to \{x \in Clsd (J) \| S \subseteq x\} \neq \emptyset$
9		ssrab2	$⊢ \{x \in Clsd (J) \| S \subseteq x\} \subseteq Clsd (J)$
10		intcld	$⊢ (\{x \in Clsd (J) \| S \subseteq x\} \neq \emptyset \land \{x \in Clsd (J) \| S \subseteq x\} \subseteq Clsd (J)) \to ⋂ \{x \in Clsd (J) \| S \subseteq x\} \in Clsd (J)$
11	8 9 10	sylancl	$⊢ (J \in Top \land S \subseteq X) \to ⋂ \{x \in Clsd (J) \| S \subseteq x\} \in Clsd (J)$
12	2 11	eqeltrd	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \in Clsd (J)$

Metamath Proof Explorer