Theorem ntrneicls00

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 2-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	ntrneicls00	|- ( ph -> ( ( I ` B ) = B <-> A. x e. B B e. ( N ` x ) ) )

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	1 2 3	ntrneiiex	|- ( ph -> I e. ( ~P B ^m ~P B ) )
5		elmapi	|- ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
6	4 5	syl	|- ( ph -> I : ~P B --> ~P B )
7	1 2 3	ntrneibex	|- ( ph -> B e. _V )
8		pwidg	|- ( B e. _V -> B e. ~P B )
9	7 8	syl	|- ( ph -> B e. ~P B )
10	6 9	ffvelcdmd	|- ( ph -> ( I ` B ) e. ~P B )
11	10	elpwid	|- ( ph -> ( I ` B ) C_ B )
12		eqss	|- ( ( I ` B ) = B <-> ( ( I ` B ) C_ B /\ B C_ ( I ` B ) ) )
13		dfss3	|- ( B C_ ( I ` B ) <-> A. x e. B x e. ( I ` B ) )
14	13	anbi2i	|- ( ( ( I ` B ) C_ B /\ B C_ ( I ` B ) ) <-> ( ( I ` B ) C_ B /\ A. x e. B x e. ( I ` B ) ) )
15	12 14	bitri	|- ( ( I ` B ) = B <-> ( ( I ` B ) C_ B /\ A. x e. B x e. ( I ` B ) ) )
16	15	a1i	|- ( ph -> ( ( I ` B ) = B <-> ( ( I ` B ) C_ B /\ A. x e. B x e. ( I ` B ) ) ) )
17	11 16	mpbirand	|- ( ph -> ( ( I ` B ) = B <-> A. x e. B x e. ( I ` B ) ) )
18	3	adantr	|- ( ( ph /\ x e. B ) -> I F N )
19		simpr	|- ( ( ph /\ x e. B ) -> x e. B )
20	9	adantr	|- ( ( ph /\ x e. B ) -> B e. ~P B )
21	1 2 18 19 20	ntrneiel	|- ( ( ph /\ x e. B ) -> ( x e. ( I ` B ) <-> B e. ( N ` x ) ) )
22	21	ralbidva	|- ( ph -> ( A. x e. B x e. ( I ` B ) <-> A. x e. B B e. ( N ` x ) ) )
23	17 22	bitrd	|- ( ph -> ( ( I ` B ) = B <-> A. x e. B B e. ( N ` x ) ) )