Theorem ntrneicnv

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then converse of F is known. (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 )
Assertion	ntrneicnv	|- ( ph -> `' F = ( B O ~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	1 2 3	ntrneibex	|- ( ph -> B e. _V )
5	4	pwexd	|- ( ph -> ~P B e. _V )
6		eqid	|- ( B O ~P B ) = ( B O ~P B )
7	1 5 4 2 6	fsovcnvd	|- ( ph -> `' F = ( B O ~P B ) )