ntrneik3

Description: The intersection of interiors of any pair is a subset of the interior of the intersection if and only if the intersection of any two neighborhoods of a point is also a neighborhood. (Contributed by RP, 19-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	ntrneik3	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \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 \in N (x)))$

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		dfss3	$⊢ I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall x \in (I (s) \cap I (t)) x \in I (s \cap t)$
5	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
6		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
7	5 6	syl	$⊢ φ \to I : 𝒫 B ⟶ 𝒫 B$
8	7	ffvelrnda	$⊢ (φ \land s \in 𝒫 B) \to I (s) \in 𝒫 B$
9	8	elpwid	$⊢ (φ \land s \in 𝒫 B) \to I (s) \subseteq B$
10		ssinss1	$⊢ I (s) \subseteq B \to I (s) \cap I (t) \subseteq B$
11	9 10	syl	$⊢ (φ \land s \in 𝒫 B) \to I (s) \cap I (t) \subseteq B$
12	11	adantr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s) \cap I (t) \subseteq B$
13		ralss	$⊢ I (s) \cap I (t) \subseteq B \to (\forall x \in (I (s) \cap I (t)) x \in I (s \cap t) \leftrightarrow \forall x \in B (x \in (I (s) \cap I (t)) \to x \in I (s \cap t)))$
14	12 13	syl	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in (I (s) \cap I (t)) x \in I (s \cap t) \leftrightarrow \forall x \in B (x \in (I (s) \cap I (t)) \to x \in I (s \cap t)))$
15		elin	$⊢ x \in (I (s) \cap I (t)) \leftrightarrow (x \in I (s) \land x \in I (t))$
16	3	ad3antrrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to I F N$
17		simpr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to x \in B$
18		simpllr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \in 𝒫 B$
19	1 2 16 17 18	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (s) \leftrightarrow s \in N (x))$
20		simplr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to t \in 𝒫 B$
21	1 2 16 17 20	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (t) \leftrightarrow t \in N (x))$
22	19 21	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)))$
23	15 22	syl5bb	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in (I (s) \cap I (t)) \leftrightarrow (s \in N (x) \land t \in N (x)))$
24	1 2 3	ntrneibex	$⊢ φ \to B \in V$
25	24	ad3antrrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to B \in V$
26	18	elpwid	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \subseteq B$
27		ssinss1	$⊢ s \subseteq B \to s \cap t \subseteq B$
28	26 27	syl	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \cap t \subseteq B$
29	25 28	sselpwd	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \cap t \in 𝒫 B$
30	1 2 16 17 29	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (s \cap t) \leftrightarrow s \cap t \in N (x))$
31	23 30	imbi12d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((x \in (I (s) \cap I (t)) \to x \in I (s \cap t)) \leftrightarrow ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)))$
32	31	ralbidva	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in B (x \in (I (s) \cap I (t)) \to x \in I (s \cap t)) \leftrightarrow \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)))$
33	14 32	bitrd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in (I (s) \cap I (t)) x \in I (s \cap t) \leftrightarrow \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)))$
34	4 33	syl5bb	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)))$
35	34	ralbidva	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall t \in 𝒫 B \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)))$
36		ralcom	$⊢ \forall t \in 𝒫 B \forall x \in B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)) \leftrightarrow \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x))$
37	35 36	bitrdi	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)))$
38	37	ralbidva	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \leftrightarrow \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)))$
39		ralcom	$⊢ \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B ((s \in N (x) \land t \in N (x)) \to s \cap t \in N (x)) \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 \in N (x))$
40	38 39	bitrdi	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t) \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 \in N (x)))$

Metamath Proof Explorer

Theorem ntrneik3

Proof