ntrval2

Description: Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007)

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

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		difss	$⊢ X ∖ S \subseteq X$
3	1	clsval2	$⊢ (J \in Top \land X ∖ S \subseteq X) \to cls (J) (X ∖ S) = X ∖ int (J) (X ∖ (X ∖ S))$
4	2 3	mpan2	$⊢ J \in Top \to cls (J) (X ∖ S) = X ∖ int (J) (X ∖ (X ∖ S))$
5	4	adantr	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (X ∖ S) = X ∖ int (J) (X ∖ (X ∖ S))$
6		dfss4	$⊢ S \subseteq X \leftrightarrow X ∖ (X ∖ S) = S$
7	6	biimpi	$⊢ S \subseteq X \to X ∖ (X ∖ S) = S$
8	7	fveq2d	$⊢ S \subseteq X \to int (J) (X ∖ (X ∖ S)) = int (J) (S)$
9	8	adantl	$⊢ (J \in Top \land S \subseteq X) \to int (J) (X ∖ (X ∖ S)) = int (J) (S)$
10	9	difeq2d	$⊢ (J \in Top \land S \subseteq X) \to X ∖ int (J) (X ∖ (X ∖ S)) = X ∖ int (J) (S)$
11	5 10	eqtrd	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (X ∖ S) = X ∖ int (J) (S)$
12	11	difeq2d	$⊢ (J \in Top \land S \subseteq X) \to X ∖ cls (J) (X ∖ S) = X ∖ (X ∖ int (J) (S))$
13	1	ntropn	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) \in J$
14	1	eltopss	$⊢ (J \in Top \land int (J) (S) \in J) \to int (J) (S) \subseteq X$
15	13 14	syldan	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) \subseteq X$
16		dfss4	$⊢ int (J) (S) \subseteq X \leftrightarrow X ∖ (X ∖ int (J) (S)) = int (J) (S)$
17	15 16	sylib	$⊢ (J \in Top \land S \subseteq X) \to X ∖ (X ∖ int (J) (S)) = int (J) (S)$
18	12 17	eqtr2d	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = X ∖ cls (J) (X ∖ S)$

Metamath Proof Explorer