ntrcls0

Description: A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007)

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

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		simpl	$⊢ (J \in Top \land S \subseteq X) \to J \in Top$
3	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
4	1	sscls	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$
5	1	ntrss	$⊢ (J \in Top \land cls (J) (S) \subseteq X \land S \subseteq cls (J) (S)) \to int (J) (S) \subseteq int (J) (cls (J) (S))$
6	2 3 4 5	syl3anc	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) \subseteq int (J) (cls (J) (S))$
7	6	3adant3	$⊢ (J \in Top \land S \subseteq X \land int (J) (cls (J) (S)) = \emptyset) \to int (J) (S) \subseteq int (J) (cls (J) (S))$
8		sseq2	$⊢ int (J) (cls (J) (S)) = \emptyset \to (int (J) (S) \subseteq int (J) (cls (J) (S)) \leftrightarrow int (J) (S) \subseteq \emptyset)$
9	8	3ad2ant3	$⊢ (J \in Top \land S \subseteq X \land int (J) (cls (J) (S)) = \emptyset) \to (int (J) (S) \subseteq int (J) (cls (J) (S)) \leftrightarrow int (J) (S) \subseteq \emptyset)$
10	7 9	mpbid	$⊢ (J \in Top \land S \subseteq X \land int (J) (cls (J) (S)) = \emptyset) \to int (J) (S) \subseteq \emptyset$
11		ss0	$⊢ int (J) (S) \subseteq \emptyset \to int (J) (S) = \emptyset$
12	10 11	syl	$⊢ (J \in Top \land S \subseteq X \land int (J) (cls (J) (S)) = \emptyset) \to int (J) (S) = \emptyset$

Metamath Proof Explorer