Metamath Proof Explorer

Theorem 0ntr

Description: A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		ssdif0	$⊢ X \subseteq S \leftrightarrow X ∖ S = \emptyset$
3		eqss	$⊢ S = X \leftrightarrow (S \subseteq X \land X \subseteq S)$
4		fveq2	$⊢ S = X \to int (J) (S) = int (J) (X)$
5	1	ntrtop	$⊢ J \in Top \to int (J) (X) = X$
6	4 5	sylan9eqr	$⊢ (J \in Top \land S = X) \to int (J) (S) = X$
7	6	eqeq1d	$⊢ (J \in Top \land S = X) \to (int (J) (S) = \emptyset \leftrightarrow X = \emptyset)$
8	7	biimpd	$⊢ (J \in Top \land S = X) \to (int (J) (S) = \emptyset \to X = \emptyset)$
9	8	ex	$⊢ J \in Top \to (S = X \to (int (J) (S) = \emptyset \to X = \emptyset))$
10	3 9	syl5bir	$⊢ J \in Top \to ((S \subseteq X \land X \subseteq S) \to (int (J) (S) = \emptyset \to X = \emptyset))$
11	10	expd	$⊢ J \in Top \to (S \subseteq X \to (X \subseteq S \to (int (J) (S) = \emptyset \to X = \emptyset)))$
12	11	com34	$⊢ J \in Top \to (S \subseteq X \to (int (J) (S) = \emptyset \to (X \subseteq S \to X = \emptyset)))$
13	12	imp32	$⊢ (J \in Top \land (S \subseteq X \land int (J) (S) = \emptyset)) \to (X \subseteq S \to X = \emptyset)$
14	2 13	syl5bir	$⊢ (J \in Top \land (S \subseteq X \land int (J) (S) = \emptyset)) \to (X ∖ S = \emptyset \to X = \emptyset)$
15	14	necon3d	$⊢ (J \in Top \land (S \subseteq X \land int (J) (S) = \emptyset)) \to (X \neq \emptyset \to X ∖ S \neq \emptyset)$
16	15	imp	$⊢ ((J \in Top \land (S \subseteq X \land int (J) (S) = \emptyset)) \land X \neq \emptyset) \to X ∖ S \neq \emptyset$
17	16	an32s	$⊢ ((J \in Top \land X \neq \emptyset) \land (S \subseteq X \land int (J) (S) = \emptyset)) \to X ∖ S \neq \emptyset$