Metamath Proof Explorer

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 ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
ntrnei.f ⊢F=𝒫BOB
ntrnei.r ⊢φ→IFN
ntrnei.x ⊢φ→X∈B
ntrnei.s ⊢φ→S∈𝒫B
Assertion ntrneiel ⊢φ→X∈I⁡S↔S∈N⁡X

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 ntrnei.f ⊢F=𝒫BOB
3 ntrnei.r ⊢φ→IFN
4 ntrnei.x ⊢φ→X∈B
5 ntrnei.s ⊢φ→S∈𝒫B
6 fveq2 ⊢m=S→I⁡m=I⁡S
7 6 eleq2d ⊢m=S→X∈I⁡m↔X∈I⁡S
8 7 elrab3 ⊢S∈𝒫B→S∈m∈𝒫B|X∈I⁡m↔X∈I⁡S
9 5 8 syl ⊢φ→S∈m∈𝒫B|X∈I⁡m↔X∈I⁡S
10 1 2 3 ntrneibex ⊢φ→B∈V
11 10 pwexd ⊢φ→𝒫B∈V
12 1 2 3 ntrneiiex ⊢φ→I∈𝒫B𝒫B
13 eqid ⊢F⁡I=F⁡I
14 1 11 10 2 12 13 4 fsovfvfvd ⊢φ→F⁡I⁡X=m∈𝒫B|X∈I⁡m
15 1 2 3 ntrneifv1 ⊢φ→F⁡I=N
16 15 fveq1d ⊢φ→F⁡I⁡X=N⁡X
17 14 16 eqtr3d ⊢φ→m∈𝒫B|X∈I⁡m=N⁡X
18 17 eleq2d ⊢φ→S∈m∈𝒫B|X∈I⁡m↔S∈N⁡X
19 9 18 bitr3d ⊢φ→X∈I⁡S↔S∈N⁡X