Theorem ntrneifv1

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the function value of F is the neighborhood function. (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	ntrneifv1	|- ( ph -> ( F ` I ) = N )

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	ntrneif1o	|- ( ph -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
5		f1ofn	|- ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> F Fn ( ~P B ^m ~P B ) )
6	4 5	syl	|- ( ph -> F Fn ( ~P B ^m ~P B ) )
7	1 2 3	ntrneiiex	|- ( ph -> I e. ( ~P B ^m ~P B ) )
8	6 7	jca	|- ( ph -> ( F Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) )
9		fnfun	|- ( F Fn ( ~P B ^m ~P B ) -> Fun F )
10	9	adantr	|- ( ( F Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) -> Fun F )
11		fndm	|- ( F Fn ( ~P B ^m ~P B ) -> dom F = ( ~P B ^m ~P B ) )
12	11	eleq2d	|- ( F Fn ( ~P B ^m ~P B ) -> ( I e. dom F <-> I e. ( ~P B ^m ~P B ) ) )
13	12	biimpar	|- ( ( F Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) -> I e. dom F )
14	10 13	jca	|- ( ( F Fn ( ~P B ^m ~P B ) /\ I e. ( ~P B ^m ~P B ) ) -> ( Fun F /\ I e. dom F ) )
15		funbrfvb	|- ( ( Fun F /\ I e. dom F ) -> ( ( F ` I ) = N <-> I F N ) )
16	8 14 15	3syl	|- ( ph -> ( ( F ` I ) = N <-> I F N ) )
17	3 16	mpbird	|- ( ph -> ( F ` I ) = N )