Metamath Proof Explorer

Theorem ntrneibex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the base set exists. (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
Assertion ntrneibex ⊢φ→B∈V

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 oveq2 ⊢i=a→𝒫ji=𝒫ja
5 rabeq ⊢i=a→m∈i|l∈k⁡m=m∈a|l∈k⁡m
6 5 mpteq2dv ⊢i=a→l∈j⟼m∈i|l∈k⁡m=l∈j⟼m∈a|l∈k⁡m
7 4 6 mpteq12dv ⊢i=a→k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m=k∈𝒫ja⟼l∈j⟼m∈a|l∈k⁡m
8 pweq ⊢j=b→𝒫j=𝒫b
9 8 oveq1d ⊢j=b→𝒫ja=𝒫ba
10 mpteq1 ⊢j=b→l∈j⟼m∈a|l∈k⁡m=l∈b⟼m∈a|l∈k⁡m
11 9 10 mpteq12dv ⊢j=b→k∈𝒫ja⟼l∈j⟼m∈a|l∈k⁡m=k∈𝒫ba⟼l∈b⟼m∈a|l∈k⁡m
12 7 11 cbvmpov ⊢i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m=a∈V,b∈V⟼k∈𝒫ba⟼l∈b⟼m∈a|l∈k⁡m
13 1 12 eqtri ⊢O=a∈V,b∈V⟼k∈𝒫ba⟼l∈b⟼m∈a|l∈k⁡m
14 2 a1i ⊢φ→F=𝒫BOB
15 13 3 14 brovmptimex2 ⊢φ→B∈V