Theorem ntrneinex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the neighborhood function exists. (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	ntrneinex	|- ( ph -> N e. ( ~P ~P B ^m 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	ntrneif1o	|- ( ph -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
5		f1orel	|- ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> Rel F )
6	4 5	syl	|- ( ph -> Rel F )
7		relelrn	|- ( ( Rel F /\ I F N ) -> N e. ran F )
8	6 3 7	syl2anc	|- ( ph -> N e. ran F )
9		dff1o2	|- ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) <-> ( F Fn ( ~P B ^m ~P B ) /\ Fun `' F /\ ran F = ( ~P ~P B ^m B ) ) )
10	4 9	sylib	|- ( ph -> ( F Fn ( ~P B ^m ~P B ) /\ Fun `' F /\ ran F = ( ~P ~P B ^m B ) ) )
11	10	simp3d	|- ( ph -> ran F = ( ~P ~P B ^m B ) )
12	8 11	eleqtrd	|- ( ph -> N e. ( ~P ~P B ^m B ) )