ntreq0

Description: Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	ntrval	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = ⋃ (J \cap 𝒫 S)$
3	2	eqeq1d	$⊢ (J \in Top \land S \subseteq X) \to (int (J) (S) = \emptyset \leftrightarrow ⋃ (J \cap 𝒫 S) = \emptyset)$
4		neq0	$⊢ \neg ⋃ (J \cap 𝒫 S) = \emptyset \leftrightarrow \exists y y \in ⋃ (J \cap 𝒫 S)$
5	4	con1bii	$⊢ \neg \exists y y \in ⋃ (J \cap 𝒫 S) \leftrightarrow ⋃ (J \cap 𝒫 S) = \emptyset$
6		ancom	$⊢ (y \in x \land x \in (J \cap 𝒫 S)) \leftrightarrow (x \in (J \cap 𝒫 S) \land y \in x)$
7		elin	$⊢ x \in (J \cap 𝒫 S) \leftrightarrow (x \in J \land x \in 𝒫 S)$
8	7	anbi1i	$⊢ (x \in (J \cap 𝒫 S) \land y \in x) \leftrightarrow ((x \in J \land x \in 𝒫 S) \land y \in x)$
9		anass	$⊢ ((x \in J \land x \in 𝒫 S) \land y \in x) \leftrightarrow (x \in J \land (x \in 𝒫 S \land y \in x))$
10	6 8 9	3bitri	$⊢ (y \in x \land x \in (J \cap 𝒫 S)) \leftrightarrow (x \in J \land (x \in 𝒫 S \land y \in x))$
11	10	exbii	$⊢ \exists x (y \in x \land x \in (J \cap 𝒫 S)) \leftrightarrow \exists x (x \in J \land (x \in 𝒫 S \land y \in x))$
12		eluni	$⊢ y \in ⋃ (J \cap 𝒫 S) \leftrightarrow \exists x (y \in x \land x \in (J \cap 𝒫 S))$
13		df-rex	$⊢ \exists x \in J (x \in 𝒫 S \land y \in x) \leftrightarrow \exists x (x \in J \land (x \in 𝒫 S \land y \in x))$
14	11 12 13	3bitr4i	$⊢ y \in ⋃ (J \cap 𝒫 S) \leftrightarrow \exists x \in J (x \in 𝒫 S \land y \in x)$
15	14	exbii	$⊢ \exists y y \in ⋃ (J \cap 𝒫 S) \leftrightarrow \exists y \exists x \in J (x \in 𝒫 S \land y \in x)$
16		rexcom4	$⊢ \exists x \in J \exists y (x \in 𝒫 S \land y \in x) \leftrightarrow \exists y \exists x \in J (x \in 𝒫 S \land y \in x)$
17		19.42v	$⊢ \exists y (x \in 𝒫 S \land y \in x) \leftrightarrow (x \in 𝒫 S \land \exists y y \in x)$
18	17	rexbii	$⊢ \exists x \in J \exists y (x \in 𝒫 S \land y \in x) \leftrightarrow \exists x \in J (x \in 𝒫 S \land \exists y y \in x)$
19	15 16 18	3bitr2i	$⊢ \exists y y \in ⋃ (J \cap 𝒫 S) \leftrightarrow \exists x \in J (x \in 𝒫 S \land \exists y y \in x)$
20	19	notbii	$⊢ \neg \exists y y \in ⋃ (J \cap 𝒫 S) \leftrightarrow \neg \exists x \in J (x \in 𝒫 S \land \exists y y \in x)$
21	5 20	bitr3i	$⊢ ⋃ (J \cap 𝒫 S) = \emptyset \leftrightarrow \neg \exists x \in J (x \in 𝒫 S \land \exists y y \in x)$
22		ralinexa	$⊢ \forall x \in J (x \in 𝒫 S \to \neg \exists y y \in x) \leftrightarrow \neg \exists x \in J (x \in 𝒫 S \land \exists y y \in x)$
23		velpw	$⊢ x \in 𝒫 S \leftrightarrow x \subseteq S$
24		neq0	$⊢ \neg x = \emptyset \leftrightarrow \exists y y \in x$
25	24	con1bii	$⊢ \neg \exists y y \in x \leftrightarrow x = \emptyset$
26	23 25	imbi12i	$⊢ (x \in 𝒫 S \to \neg \exists y y \in x) \leftrightarrow (x \subseteq S \to x = \emptyset)$
27	26	ralbii	$⊢ \forall x \in J (x \in 𝒫 S \to \neg \exists y y \in x) \leftrightarrow \forall x \in J (x \subseteq S \to x = \emptyset)$
28	21 22 27	3bitr2i	$⊢ ⋃ (J \cap 𝒫 S) = \emptyset \leftrightarrow \forall x \in J (x \subseteq S \to x = \emptyset)$
29	3 28	bitrdi	$⊢ (J \in Top \land S \subseteq X) \to (int (J) (S) = \emptyset \leftrightarrow \forall x \in J (x \subseteq S \to x = \emptyset))$

Metamath Proof Explorer

Theorem ntreq0

Proof