iscld4

Description: A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008)

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

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	iscld3	$⊢ (J \in Top \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) = S)$
3		eqss	$⊢ cls (J) (S) = S \leftrightarrow (cls (J) (S) \subseteq S \land S \subseteq cls (J) (S))$
4	1	sscls	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$
5	4	biantrud	$⊢ (J \in Top \land S \subseteq X) \to (cls (J) (S) \subseteq S \leftrightarrow (cls (J) (S) \subseteq S \land S \subseteq cls (J) (S)))$
6	3 5	bitr4id	$⊢ (J \in Top \land S \subseteq X) \to (cls (J) (S) = S \leftrightarrow cls (J) (S) \subseteq S)$
7	2 6	bitrd	$⊢ (J \in Top \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) \subseteq S)$

Metamath Proof Explorer