ntrneifv3

Description: The value of the neighbors (convergents) expressed in terms of the interior (closure) function. (Contributed by RP, 26-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$
	ntrnei.x	$⊢ φ \to X \in B$
Assertion	ntrneifv3	$⊢ φ \to N (X) = \{s \in 𝒫 B \| X \in I (s)\}$

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		ntrnei.x	$⊢ φ \to X \in B$
5		dfin5	$⊢ 𝒫 B \cap N (X) = \{s \in 𝒫 B \| s \in N (X)\}$
6	1 2 3	ntrneinex	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$
7		elmapi	$⊢ N \in ({𝒫 𝒫 B}^{B}) \to N : B ⟶ 𝒫 𝒫 B$
8	6 7	syl	$⊢ φ \to N : B ⟶ 𝒫 𝒫 B$
9	8 4	ffvelcdmd	$⊢ φ \to N (X) \in 𝒫 𝒫 B$
10	9	elpwid	$⊢ φ \to N (X) \subseteq 𝒫 B$
11		sseqin2	$⊢ N (X) \subseteq 𝒫 B \leftrightarrow 𝒫 B \cap N (X) = N (X)$
12	10 11	sylib	$⊢ φ \to 𝒫 B \cap N (X) = N (X)$
13	3	adantr	$⊢ (φ \land s \in 𝒫 B) \to I F N$
14	4	adantr	$⊢ (φ \land s \in 𝒫 B) \to X \in B$
15		simpr	$⊢ (φ \land s \in 𝒫 B) \to s \in 𝒫 B$
16	1 2 13 14 15	ntrneiel	$⊢ (φ \land s \in 𝒫 B) \to (X \in I (s) \leftrightarrow s \in N (X))$
17	16	bicomd	$⊢ (φ \land s \in 𝒫 B) \to (s \in N (X) \leftrightarrow X \in I (s))$
18	17	rabbidva	$⊢ φ \to \{s \in 𝒫 B \| s \in N (X)\} = \{s \in 𝒫 B \| X \in I (s)\}$
19	5 12 18	3eqtr3a	$⊢ φ \to N (X) = \{s \in 𝒫 B \| X \in I (s)\}$

Metamath Proof Explorer