isopn2

Description: A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006)

		Ref	Expression
	Hypothesis	iscld.1	$⊢ X = ⋃ J$
	Assertion	isopn2	$⊢ (J \in Top \land S \subseteq X) \to (S \in J \leftrightarrow X ∖ S \in Clsd (J))$

Step	Hyp	Ref	Expression
1		iscld.1	$⊢ X = ⋃ J$
2		difss	$⊢ X ∖ S \subseteq X$
3	1	iscld2	$⊢ (J \in Top \land X ∖ S \subseteq X) \to (X ∖ S \in Clsd (J) \leftrightarrow X ∖ (X ∖ S) \in J)$
4	2 3	mpan2	$⊢ J \in Top \to (X ∖ S \in Clsd (J) \leftrightarrow X ∖ (X ∖ S) \in J)$
5		dfss4	$⊢ S \subseteq X \leftrightarrow X ∖ (X ∖ S) = S$
6	5	biimpi	$⊢ S \subseteq X \to X ∖ (X ∖ S) = S$
7	6	eleq1d	$⊢ S \subseteq X \to (X ∖ (X ∖ S) \in J \leftrightarrow S \in J)$
8	4 7	sylan9bb	$⊢ (J \in Top \land S \subseteq X) \to (X ∖ S \in Clsd (J) \leftrightarrow S \in J)$
9	8	bicomd	$⊢ (J \in Top \land S \subseteq X) \to (S \in J \leftrightarrow X ∖ S \in Clsd (J))$

Metamath Proof Explorer