ntrneiel2

Description: Membership in iterated interior of a set is equivalent to there existing a particular neighborhood of that member such that points are members of that neighborhood if and only if the set is a neighborhood of each of those points. (Contributed by RP, 11-Jul-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$
	ntrneiel2.x	$⊢ φ \to X \in B$
	ntrneiel2.s	$⊢ φ \to S \in 𝒫 B$
Assertion	ntrneiel2	$⊢ φ \to (X \in I (I (S)) \leftrightarrow \exists u \in N (X) \forall y \in B (y \in u \leftrightarrow S \in N (y)))$

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		ntrneiel2.x	$⊢ φ \to X \in B$
5		ntrneiel2.s	$⊢ φ \to S \in 𝒫 B$
6	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
7		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
8	6 7	syl	$⊢ φ \to I : 𝒫 B ⟶ 𝒫 B$
9	8 5	ffvelrnd	$⊢ φ \to I (S) \in 𝒫 B$
10	1 2 3 4 9	ntrneiel	$⊢ φ \to (X \in I (I (S)) \leftrightarrow I (S) \in N (X))$
11	1 2 3 5	ntrneifv4	$⊢ φ \to I (S) = \{y \in B \| S \in N (y)\}$
12		df-rab	$⊢ \{y \in B \| S \in N (y)\} = \{y \| (y \in B \land S \in N (y))\}$
13	11 12	eqtrdi	$⊢ φ \to I (S) = \{y \| (y \in B \land S \in N (y))\}$
14	13	eleq1d	$⊢ φ \to (I (S) \in N (X) \leftrightarrow \{y \| (y \in B \land S \in N (y))\} \in N (X))$
15		clabel	$⊢ \{y \| (y \in B \land S \in N (y))\} \in N (X) \leftrightarrow \exists u (u \in N (X) \land \forall y (y \in u \leftrightarrow (y \in B \land S \in N (y))))$
16		df-rex	$⊢ \exists u \in N (X) \forall y (y \in u \leftrightarrow (y \in B \land S \in N (y))) \leftrightarrow \exists u (u \in N (X) \land \forall y (y \in u \leftrightarrow (y \in B \land S \in N (y))))$
17	15 16	bitr4i	$⊢ \{y \| (y \in B \land S \in N (y))\} \in N (X) \leftrightarrow \exists u \in N (X) \forall y (y \in u \leftrightarrow (y \in B \land S \in N (y)))$
18		ibar	$⊢ y \in B \to (S \in N (y) \leftrightarrow (y \in B \land S \in N (y)))$
19	18	bibi2d	$⊢ y \in B \to ((y \in u \leftrightarrow S \in N (y)) \leftrightarrow (y \in u \leftrightarrow (y \in B \land S \in N (y))))$
20	19	ralbiia	$⊢ \forall y \in B (y \in u \leftrightarrow S \in N (y)) \leftrightarrow \forall y \in B (y \in u \leftrightarrow (y \in B \land S \in N (y)))$
21		ssv	$⊢ B \subseteq V$
22	21	a1i	$⊢ (φ \land u \in N (X)) \to B \subseteq V$
23		vex	$⊢ y \in V$
24		eldif	$⊢ y \in (V ∖ B) \leftrightarrow (y \in V \land \neg y \in B)$
25	23 24	mpbiran	$⊢ y \in (V ∖ B) \leftrightarrow \neg y \in B$
26	1 2 3	ntrneinex	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$
27		elmapi	$⊢ N \in ({𝒫 𝒫 B}^{B}) \to N : B ⟶ 𝒫 𝒫 B$
28	26 27	syl	$⊢ φ \to N : B ⟶ 𝒫 𝒫 B$
29	28 4	ffvelrnd	$⊢ φ \to N (X) \in 𝒫 𝒫 B$
30	29	elpwid	$⊢ φ \to N (X) \subseteq 𝒫 B$
31	30	sselda	$⊢ (φ \land u \in N (X)) \to u \in 𝒫 B$
32	31	elpwid	$⊢ (φ \land u \in N (X)) \to u \subseteq B$
33	32	sseld	$⊢ (φ \land u \in N (X)) \to (y \in u \to y \in B)$
34	33	con3dimp	$⊢ ((φ \land u \in N (X)) \land \neg y \in B) \to \neg y \in u$
35		pm3.14	$⊢ (\neg y \in B \lor \neg S \in N (y)) \to \neg (y \in B \land S \in N (y))$
36	35	orcs	$⊢ \neg y \in B \to \neg (y \in B \land S \in N (y))$
37	36	adantl	$⊢ ((φ \land u \in N (X)) \land \neg y \in B) \to \neg (y \in B \land S \in N (y))$
38	34 37	2falsed	$⊢ ((φ \land u \in N (X)) \land \neg y \in B) \to (y \in u \leftrightarrow (y \in B \land S \in N (y)))$
39	38	ex	$⊢ (φ \land u \in N (X)) \to (\neg y \in B \to (y \in u \leftrightarrow (y \in B \land S \in N (y))))$
40	25 39	syl5bi	$⊢ (φ \land u \in N (X)) \to (y \in (V ∖ B) \to (y \in u \leftrightarrow (y \in B \land S \in N (y))))$
41	40	ralrimiv	$⊢ (φ \land u \in N (X)) \to \forall y \in (V ∖ B) (y \in u \leftrightarrow (y \in B \land S \in N (y)))$
42	22 41	raldifeq	$⊢ (φ \land u \in N (X)) \to (\forall y \in B (y \in u \leftrightarrow (y \in B \land S \in N (y))) \leftrightarrow \forall y \in V (y \in u \leftrightarrow (y \in B \land S \in N (y))))$
43	20 42	syl5bb	$⊢ (φ \land u \in N (X)) \to (\forall y \in B (y \in u \leftrightarrow S \in N (y)) \leftrightarrow \forall y \in V (y \in u \leftrightarrow (y \in B \land S \in N (y))))$
44		ralv	$⊢ \forall y \in V (y \in u \leftrightarrow (y \in B \land S \in N (y))) \leftrightarrow \forall y (y \in u \leftrightarrow (y \in B \land S \in N (y)))$
45	43 44	bitr2di	$⊢ (φ \land u \in N (X)) \to (\forall y (y \in u \leftrightarrow (y \in B \land S \in N (y))) \leftrightarrow \forall y \in B (y \in u \leftrightarrow S \in N (y)))$
46	45	rexbidva	$⊢ φ \to (\exists u \in N (X) \forall y (y \in u \leftrightarrow (y \in B \land S \in N (y))) \leftrightarrow \exists u \in N (X) \forall y \in B (y \in u \leftrightarrow S \in N (y)))$
47	17 46	syl5bb	$⊢ φ \to (\{y \| (y \in B \land S \in N (y))\} \in N (X) \leftrightarrow \exists u \in N (X) \forall y \in B (y \in u \leftrightarrow S \in N (y)))$
48	10 14 47	3bitrd	$⊢ φ \to (X \in I (I (S)) \leftrightarrow \exists u \in N (X) \forall y \in B (y \in u \leftrightarrow S \in N (y)))$

Metamath Proof Explorer

Theorem ntrneiel2

Proof