ntrneikb

Description: The interiors of disjoint sets are disjoint if and only if the neighborhoods of every point contain no disjoint sets. (Contributed by RP, 11-Jun-2021)

	Ref	Expression
Hypotheses	ntrnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
	ntrnei.f	$⊢ F = 𝒫 B O B$
	ntrnei.r	$⊢ φ \to I F N$
Assertion	ntrneikb	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
2		ntrnei.f	$⊢ F = 𝒫 B O B$
3		ntrnei.r	$⊢ φ \to I F N$
4		con34b	$⊢ ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow (\neg s \cap t \neq \emptyset \to \neg (x \in I (s) \land x \in I (t)))$
5	4	albii	$⊢ \forall x ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow \forall x (\neg s \cap t \neq \emptyset \to \neg (x \in I (s) \land x \in I (t)))$
6		19.21v	$⊢ \forall x (\neg s \cap t \neq \emptyset \to \neg (x \in I (s) \land x \in I (t))) \leftrightarrow (\neg s \cap t \neq \emptyset \to \forall x \neg (x \in I (s) \land x \in I (t)))$
7		nne	$⊢ \neg s \cap t \neq \emptyset \leftrightarrow s \cap t = \emptyset$
8		elin	$⊢ x \in (I (s) \cap I (t)) \leftrightarrow (x \in I (s) \land x \in I (t))$
9	8	imbi1i	$⊢ (x \in (I (s) \cap I (t)) \to x \in \emptyset) \leftrightarrow ((x \in I (s) \land x \in I (t)) \to x \in \emptyset)$
10		noel	$⊢ \neg x \in \emptyset$
11		imnot	$⊢ \neg x \in \emptyset \to (((x \in I (s) \land x \in I (t)) \to x \in \emptyset) \leftrightarrow \neg (x \in I (s) \land x \in I (t)))$
12	10 11	ax-mp	$⊢ ((x \in I (s) \land x \in I (t)) \to x \in \emptyset) \leftrightarrow \neg (x \in I (s) \land x \in I (t))$
13	9 12	bitr2i	$⊢ \neg (x \in I (s) \land x \in I (t)) \leftrightarrow (x \in (I (s) \cap I (t)) \to x \in \emptyset)$
14	13	albii	$⊢ \forall x \neg (x \in I (s) \land x \in I (t)) \leftrightarrow \forall x (x \in (I (s) \cap I (t)) \to x \in \emptyset)$
15		df-ss	$⊢ I (s) \cap I (t) \subseteq \emptyset \leftrightarrow \forall x (x \in (I (s) \cap I (t)) \to x \in \emptyset)$
16		ss0b	$⊢ I (s) \cap I (t) \subseteq \emptyset \leftrightarrow I (s) \cap I (t) = \emptyset$
17	14 15 16	3bitr2i	$⊢ \forall x \neg (x \in I (s) \land x \in I (t)) \leftrightarrow I (s) \cap I (t) = \emptyset$
18	7 17	imbi12i	$⊢ (\neg s \cap t \neq \emptyset \to \forall x \neg (x \in I (s) \land x \in I (t))) \leftrightarrow (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset)$
19	5 6 18	3bitrri	$⊢ (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall x ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset)$
20	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
21		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
22	20 21	syl	$⊢ φ \to I : 𝒫 B ⟶ 𝒫 B$
23	22	ffvelcdmda	$⊢ (φ \land s \in 𝒫 B) \to I (s) \in 𝒫 B$
24	23	adantr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s) \in 𝒫 B$
25	24	elpwid	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s) \subseteq B$
26	25	sseld	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (x \in I (s) \to x \in B)$
27	26	adantrd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to ((x \in I (s) \land x \in I (t)) \to x \in B)$
28	27	imp	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land (x \in I (s) \land x \in I (t))) \to x \in B$
29		biimt	$⊢ x \in B \to (s \cap t \neq \emptyset \leftrightarrow (x \in B \to s \cap t \neq \emptyset))$
30	28 29	syl	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land (x \in I (s) \land x \in I (t))) \to (s \cap t \neq \emptyset \leftrightarrow (x \in B \to s \cap t \neq \emptyset))$
31	30	pm5.74da	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow ((x \in I (s) \land x \in I (t)) \to (x \in B \to s \cap t \neq \emptyset)))$
32		bi2.04	$⊢ ((x \in I (s) \land x \in I (t)) \to (x \in B \to s \cap t \neq \emptyset)) \leftrightarrow (x \in B \to ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset))$
33	31 32	bitrdi	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow (x \in B \to ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset)))$
34	33	albidv	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow \forall x (x \in B \to ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset)))$
35		df-ral	$⊢ \forall x \in B ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow \forall x (x \in B \to ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset))$
36	34 35	bitr4di	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow \forall x \in B ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset))$
37	3	ad3antrrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to I F N$
38		simpr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to x \in B$
39		simpllr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \in 𝒫 B$
40	1 2 37 38 39	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (s) \leftrightarrow s \in N (x))$
41		simplr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to t \in 𝒫 B$
42	1 2 37 38 41	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (t) \leftrightarrow t \in N (x))$
43	40 42	anbi12d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((x \in I (s) \land x \in I (t)) \leftrightarrow (s \in N (x) \land t \in N (x)))$
44	43	imbi1d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$
45	44	ralbidva	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in B ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$
46	36 45	bitrd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x ((x \in I (s) \land x \in I (t)) \to s \cap t \neq \emptyset) \leftrightarrow \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$
47	19 46	bitrid	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to ((s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$
48	47	ralbidva	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall t \in 𝒫 B \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$
49	48	ralbidva	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$
50		ralrot3	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset)$
51	49 50	bitrdi	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t = \emptyset \to I (s) \cap I (t) = \emptyset) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B ((s \in N (x) \land t \in N (x)) \to s \cap t \neq \emptyset))$

Metamath Proof Explorer

Theorem ntrneikb

Proof