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	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
	ntrneifv.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
Assertion	ntrneifv4	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ 𝑆 ∈ ( 𝑁 ‘ 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		ntrneifv.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
5		dfin5	⊢ ( 𝐵 ∩ ( 𝐼 ‘ 𝑆 ) ) = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ ( 𝐼 ‘ 𝑆 ) }
6	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
8	6 7	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
9	8 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) ∈ 𝒫 𝐵 )
10	9	elpwid	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) ⊆ 𝐵 )
11		sseqin2	⊢ ( ( 𝐼 ‘ 𝑆 ) ⊆ 𝐵 ↔ ( 𝐵 ∩ ( 𝐼 ‘ 𝑆 ) ) = ( 𝐼 ‘ 𝑆 ) )
12	10 11	sylib	⊢ ( 𝜑 → ( 𝐵 ∩ ( 𝐼 ‘ 𝑆 ) ) = ( 𝐼 ‘ 𝑆 ) )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
15	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
16	1 2 13 14 15	ntrneiel	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑆 ) ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑥 ) ) )
17	16	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ ( 𝐼 ‘ 𝑆 ) } = { 𝑥 ∈ 𝐵 ∣ 𝑆 ∈ ( 𝑁 ‘ 𝑥 ) } )
18	5 12 17	3eqtr3a	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ 𝑆 ∈ ( 𝑁 ‘ 𝑥 ) } )