cmclsopn

Description: The complement of a closure is open. (Contributed by NM, 11-Sep-2006)

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

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	clsval2	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = X ∖ int (J) (X ∖ S)$
3	2	difeq2d	$⊢ (J \in Top \land S \subseteq X) \to X ∖ cls (J) (S) = X ∖ (X ∖ int (J) (X ∖ S))$
4		difss	$⊢ X ∖ S \subseteq X$
5	1	ntropn	$⊢ (J \in Top \land X ∖ S \subseteq X) \to int (J) (X ∖ S) \in J$
6	4 5	mpan2	$⊢ J \in Top \to int (J) (X ∖ S) \in J$
7	1	eltopss	$⊢ (J \in Top \land int (J) (X ∖ S) \in J) \to int (J) (X ∖ S) \subseteq X$
8	6 7	mpdan	$⊢ J \in Top \to int (J) (X ∖ S) \subseteq X$
9		dfss4	$⊢ int (J) (X ∖ S) \subseteq X \leftrightarrow X ∖ (X ∖ int (J) (X ∖ S)) = int (J) (X ∖ S)$
10	8 9	sylib	$⊢ J \in Top \to X ∖ (X ∖ int (J) (X ∖ S)) = int (J) (X ∖ S)$
11	10 6	eqeltrd	$⊢ J \in Top \to X ∖ (X ∖ int (J) (X ∖ S)) \in J$
12	11	adantr	$⊢ (J \in Top \land S \subseteq X) \to X ∖ (X ∖ int (J) (X ∖ S)) \in J$
13	3 12	eqeltrd	$⊢ (J \in Top \land S \subseteq X) \to X ∖ cls (J) (S) \in J$

Metamath Proof Explorer