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 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 )
	ntrnei.x	|- ( ph -> X e. B )
	ntrnei.s	|- ( ph -> S e. ~P B )
Assertion	ntrneiel	|- ( ph -> ( X e. ( I ` S ) <-> S 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		ntrnei.x	|- ( ph -> X e. B )
5		ntrnei.s	|- ( ph -> S e. ~P B )
6		fveq2	|- ( m = S -> ( I ` m ) = ( I ` S ) )
7	6	eleq2d	|- ( m = S -> ( X e. ( I ` m ) <-> X e. ( I ` S ) ) )
8	7	elrab3	|- ( S e. ~P B -> ( S e. { m e. ~P B | X e. ( I ` m ) } <-> X e. ( I ` S ) ) )
9	5 8	syl	|- ( ph -> ( S e. { m e. ~P B | X e. ( I ` m ) } <-> X e. ( I ` S ) ) )
10	1 2 3	ntrneibex	|- ( ph -> B e. _V )
11	10	pwexd	|- ( ph -> ~P B e. _V )
12	1 2 3	ntrneiiex	|- ( ph -> I e. ( ~P B ^m ~P B ) )
13		eqid	|- ( F ` I ) = ( F ` I )
14	1 11 10 2 12 13 4	fsovfvfvd	|- ( ph -> ( ( F ` I ) ` X ) = { m e. ~P B | X e. ( I ` m ) } )
15	1 2 3	ntrneifv1	|- ( ph -> ( F ` I ) = N )
16	15	fveq1d	|- ( ph -> ( ( F ` I ) ` X ) = ( N ` X ) )
17	14 16	eqtr3d	|- ( ph -> { m e. ~P B | X e. ( I ` m ) } = ( N ` X ) )
18	17	eleq2d	|- ( ph -> ( S e. { m e. ~P B | X e. ( I ` m ) } <-> S e. ( N ` X ) ) )
19	9 18	bitr3d	|- ( ph -> ( X e. ( I ` S ) <-> S e. ( N ` X ) ) )