Theorem ntrneiel

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 29-May-2021)

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
	ntrnei.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ntrnei.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
Assertion	ntrneiel	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		ntrnei.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		ntrnei.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
6		fveq2	⊢ ( 𝑚 = 𝑆 → ( 𝐼 ‘ 𝑚 ) = ( 𝐼 ‘ 𝑆 ) )
7	6	eleq2d	⊢ ( 𝑚 = 𝑆 → ( 𝑋 ∈ ( 𝐼 ‘ 𝑚 ) ↔ 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ) )
8	7	elrab3	⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑆 ∈ { 𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ ( 𝐼 ‘ 𝑚 ) } ↔ 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ) )
9	5 8	syl	⊢ ( 𝜑 → ( 𝑆 ∈ { 𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ ( 𝐼 ‘ 𝑚 ) } ↔ 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ) )
10	1 2 3	ntrneibex	⊢ ( 𝜑 → 𝐵 ∈ V )
11	10	pwexd	⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
12	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
13		eqid	⊢ ( 𝐹 ‘ 𝐼 ) = ( 𝐹 ‘ 𝐼 )
14	1 11 10 2 12 13 4	fsovfvfvd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ ( 𝐼 ‘ 𝑚 ) } )
15	1 2 3	ntrneifv1	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) = 𝑁 )
16	15	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐼 ) ‘ 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
17	14 16	eqtr3d	⊢ ( 𝜑 → { 𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ ( 𝐼 ‘ 𝑚 ) } = ( 𝑁 ‘ 𝑋 ) )
18	17	eleq2d	⊢ ( 𝜑 → ( 𝑆 ∈ { 𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ ( 𝐼 ‘ 𝑚 ) } ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ) )
19	9 18	bitr3d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑋 ) ) )