Theorem ntrclsneine0

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 21-May-2021)

	Ref	Expression
Hypotheses	ntrcls.o	|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
	ntrcls.d	|- D = ( O ` B )
	ntrcls.r	|- ( ph -> I D K )
Assertion	ntrclsneine0	|- ( ph -> ( A. x e. B E. s e. ~P B x e. ( I ` s ) <-> A. x e. B E. s e. ~P B -. x e. ( K ` s ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2		ntrcls.d	|- D = ( O ` B )
3		ntrcls.r	|- ( ph -> I D K )
4	3	adantr	|- ( ( ph /\ x e. B ) -> I D K )
5		simpr	|- ( ( ph /\ x e. B ) -> x e. B )
6	1 2 4 5	ntrclsneine0lem	|- ( ( ph /\ x e. B ) -> ( E. s e. ~P B x e. ( I ` s ) <-> E. s e. ~P B -. x e. ( K ` s ) ) )
7	6	ralbidva	|- ( ph -> ( A. x e. B E. s e. ~P B x e. ( I ` s ) <-> A. x e. B E. s e. ~P B -. x e. ( K ` s ) ) )