Metamath Proof Explorer


Theorem ntrneineine1

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-2021)

Ref Expression
Hypotheses ntrnei.o
|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
ntrnei.f
|- F = ( ~P B O B )
ntrnei.r
|- ( ph -> I F N )
Assertion ntrneineine1
|- ( ph -> ( A. x e. B E. s e. ~P B -. x e. ( I ` s ) <-> A. x e. B ( N ` x ) =/= ~P B ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o
 |-  O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
2 ntrnei.f
 |-  F = ( ~P B O B )
3 ntrnei.r
 |-  ( ph -> I F N )
4 3 adantr
 |-  ( ( ph /\ x e. B ) -> I F N )
5 simpr
 |-  ( ( ph /\ x e. B ) -> x e. B )
6 1 2 4 5 ntrneineine1lem
 |-  ( ( ph /\ x e. B ) -> ( E. s e. ~P B -. x e. ( I ` s ) <-> ( N ` x ) =/= ~P B ) )
7 6 ralbidva
 |-  ( ph -> ( A. x e. B E. s e. ~P B -. x e. ( I ` s ) <-> A. x e. B ( N ` x ) =/= ~P B ) )