Theorem ntrneifv4

Description: The value of the interior (closure) expressed in terms of the neighbors (convergents) function. (Contributed by RP, 26-Jun-2021)

	Ref	Expression
Hypotheses	ntrnei.o	$$⊢O=\left(i\in \mathrm{V},j\in \mathrm{V}⟼\left(k\in \left({𝒫j}^i\right)⟼\left(l\in j⟼\left\{m\in i|l\in k\left(m\right)\right\}\right)\right)\right)$$
	ntrnei.f	$$⊢F=𝒫BOB$$
	ntrnei.r	$$⊢\phi \to IFN$$
	ntrneifv.s	$$⊢\phi \to S\in 𝒫B$$
Assertion	ntrneifv4	$$⊢\phi \to I\left(S\right)=\left\{x\in B|S\in N\left(x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	$$⊢O=\left(i\in \mathrm{V},j\in \mathrm{V}⟼\left(k\in \left({𝒫j}^i\right)⟼\left(l\in j⟼\left\{m\in i|l\in k\left(m\right)\right\}\right)\right)\right)$$
2		ntrnei.f	$$⊢F=𝒫BOB$$
3		ntrnei.r	$$⊢\phi \to IFN$$
4		ntrneifv.s	$$⊢\phi \to S\in 𝒫B$$
5		dfin5	$$⊢B\cap I\left(S\right)=\left\{x\in B|x\in I\left(S\right)\right\}$$
6	1 2 3	ntrneiiex	$$⊢\phi \to I\in \left({𝒫B}^{𝒫B}\right)$$
7		elmapi	$$⊢I\in \left({𝒫B}^{𝒫B}\right)\to I:𝒫B⟶𝒫B$$
8	6 7	syl	$$⊢\phi \to I:𝒫B⟶𝒫B$$
9	8 4	ffvelrnd	$$⊢\phi \to I\left(S\right)\in 𝒫B$$
10	9	elpwid	$$⊢\phi \to I\left(S\right)\subseteq B$$
11		sseqin2	$$⊢I\left(S\right)\subseteq B\leftrightarrow B\cap I\left(S\right)=I\left(S\right)$$
12	10 11	sylib	$$⊢\phi \to B\cap I\left(S\right)=I\left(S\right)$$
13	3	adantr	$$⊢\left(\phi \wedge x\in B\right)\to IFN$$
14		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
15	4	adantr	$$⊢\left(\phi \wedge x\in B\right)\to S\in 𝒫B$$
16	1 2 13 14 15	ntrneiel	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\in I\left(S\right)\leftrightarrow S\in N\left(x\right)\right)$$
17	16	rabbidva	$$⊢\phi \to \left\{x\in B|x\in I\left(S\right)\right\}=\left\{x\in B|S\in N\left(x\right)\right\}$$
18	5 12 17	3eqtr3a	$$⊢\phi \to I\left(S\right)=\left\{x\in B|S\in N\left(x\right)\right\}$$