ntrneik13

Description: The interior of the intersection of any pair equals intersection of interiors if and only if the intersection of any pair belonging to the neighborhood of a point is equivalent to both of the pair belonging to the neighborhood of that point. (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	ntrneik13	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land 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 t) \subseteq I (s) \cap I (t) \leftrightarrow \forall x \in I (s \cap t) x \in (I (s) \cap I (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	ad2antrr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I : 𝒫 B ⟶ 𝒫 B$
9	1 2 3	ntrneibex	$⊢ φ \to B \in V$
10	9	ad2antrr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to B \in V$
11		simplr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \in 𝒫 B$
12		elpwi	$⊢ s \in 𝒫 B \to s \subseteq B$
13		ssinss1	$⊢ s \subseteq B \to s \cap t \subseteq B$
14	11 12 13	3syl	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \cap t \subseteq B$
15	10 14	sselpwd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \cap t \in 𝒫 B$
16	8 15	ffvelrnd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s \cap t) \in 𝒫 B$
17	16	elpwid	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s \cap t) \subseteq B$
18		ralss	$⊢ I (s \cap t) \subseteq B \to (\forall x \in I (s \cap t) x \in (I (s) \cap I (t)) \leftrightarrow \forall x \in B (x \in I (s \cap t) \to x \in (I (s) \cap I (t))))$
19	17 18	syl	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in I (s \cap t) x \in (I (s) \cap I (t)) \leftrightarrow \forall x \in B (x \in I (s \cap t) \to x \in (I (s) \cap I (t))))$
20	4 19	syl5bb	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (I (s \cap t) \subseteq I (s) \cap I (t) \leftrightarrow \forall x \in B (x \in I (s \cap t) \to x \in (I (s) \cap I (t))))$
21		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)$
22	7	ffvelrnda	$⊢ (φ \land s \in 𝒫 B) \to I (s) \in 𝒫 B$
23	22	elpwid	$⊢ (φ \land s \in 𝒫 B) \to I (s) \subseteq B$
24		ssinss1	$⊢ I (s) \subseteq B \to I (s) \cap I (t) \subseteq B$
25	23 24	syl	$⊢ (φ \land s \in 𝒫 B) \to I (s) \cap I (t) \subseteq B$
26	25	adantr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s) \cap I (t) \subseteq B$
27		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)))$
28	26 27	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)))$
29	21 28	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 (x \in (I (s) \cap I (t)) \to x \in I (s \cap t)))$
30	20 29	anbi12d	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to ((I (s \cap t) \subseteq I (s) \cap I (t) \land I (s) \cap I (t) \subseteq I (s \cap t)) \leftrightarrow (\forall x \in B (x \in I (s \cap t) \to x \in (I (s) \cap I (t))) \land \forall x \in B (x \in (I (s) \cap I (t)) \to x \in I (s \cap t))))$
31		eqss	$⊢ I (s \cap t) = I (s) \cap I (t) \leftrightarrow (I (s \cap t) \subseteq I (s) \cap I (t) \land I (s) \cap I (t) \subseteq I (s \cap t))$
32		ralbiim	$⊢ \forall x \in B (x \in I (s \cap t) \leftrightarrow x \in (I (s) \cap I (t))) \leftrightarrow (\forall x \in B (x \in I (s \cap t) \to x \in (I (s) \cap I (t))) \land \forall x \in B (x \in (I (s) \cap I (t)) \to x \in I (s \cap t)))$
33	30 31 32	3bitr4g	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall x \in B (x \in I (s \cap t) \leftrightarrow x \in (I (s) \cap I (t))))$
34	3	ad3antrrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to I F N$
35		simpr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to x \in B$
36	9	adantr	$⊢ (φ \land s \in 𝒫 B) \to B \in V$
37		simpr	$⊢ (φ \land s \in 𝒫 B) \to s \in 𝒫 B$
38	37	elpwid	$⊢ (φ \land s \in 𝒫 B) \to s \subseteq B$
39	38 13	syl	$⊢ (φ \land s \in 𝒫 B) \to s \cap t \subseteq B$
40	36 39	sselpwd	$⊢ (φ \land s \in 𝒫 B) \to s \cap t \in 𝒫 B$
41	40	ad2antrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \cap t \in 𝒫 B$
42	1 2 34 35 41	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))$
43		elin	$⊢ x \in (I (s) \cap I (t)) \leftrightarrow (x \in I (s) \land x \in I (t))$
44		simpllr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \in 𝒫 B$
45	1 2 34 35 44	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (s) \leftrightarrow s \in N (x))$
46		simplr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to t \in 𝒫 B$
47	1 2 34 35 46	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (t) \leftrightarrow t \in N (x))$
48	45 47	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)))$
49	43 48	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)))$
50	42 49	bibi12d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((x \in I (s \cap t) \leftrightarrow x \in (I (s) \cap I (t))) \leftrightarrow (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))))$
51	50	ralbidva	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in B (x \in I (s \cap t) \leftrightarrow x \in (I (s) \cap I (t))) \leftrightarrow \forall x \in B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))))$
52	33 51	bitrd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall x \in B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))))$
53	52	ralbidva	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall t \in 𝒫 B \forall x \in B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))))$
54		ralcom	$⊢ \forall t \in 𝒫 B \forall x \in B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))) \leftrightarrow \forall x \in B \forall t \in 𝒫 B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x)))$
55	53 54	bitrdi	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall x \in B \forall t \in 𝒫 B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))))$
56	55	ralbidva	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))))$
57		ralcom	$⊢ \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x)))$
58	56 57	bitrdi	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cap t \in N (x) \leftrightarrow (s \in N (x) \land t \in N (x))))$

Metamath Proof Explorer

Theorem ntrneik13

Proof