Theorem ntrneibex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the base set 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	ntrneibex	|- ( ph -> B e. _V )

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		oveq2	|- ( i = a -> ( ~P j ^m i ) = ( ~P j ^m a ) )
5		rabeq	|- ( i = a -> { m e. i | l e. ( k ` m ) } = { m e. a | l e. ( k ` m ) } )
6	5	mpteq2dv	|- ( i = a -> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) = ( l e. j |-> { m e. a | l e. ( k ` m ) } ) )
7	4 6	mpteq12dv	|- ( i = a -> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) = ( k e. ( ~P j ^m a ) |-> ( l e. j |-> { m e. a | l e. ( k ` m ) } ) ) )
8		pweq	|- ( j = b -> ~P j = ~P b )
9	8	oveq1d	|- ( j = b -> ( ~P j ^m a ) = ( ~P b ^m a ) )
10		mpteq1	|- ( j = b -> ( l e. j |-> { m e. a | l e. ( k ` m ) } ) = ( l e. b |-> { m e. a | l e. ( k ` m ) } ) )
11	9 10	mpteq12dv	|- ( j = b -> ( k e. ( ~P j ^m a ) |-> ( l e. j |-> { m e. a | l e. ( k ` m ) } ) ) = ( k e. ( ~P b ^m a ) |-> ( l e. b |-> { m e. a | l e. ( k ` m ) } ) ) )
12	7 11	cbvmpov	|- ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) ) = ( a e. _V , b e. _V |-> ( k e. ( ~P b ^m a ) |-> ( l e. b |-> { m e. a | l e. ( k ` m ) } ) ) )
13	1 12	eqtri	|- O = ( a e. _V , b e. _V |-> ( k e. ( ~P b ^m a ) |-> ( l e. b |-> { m e. a | l e. ( k ` m ) } ) ) )
14	2	a1i	|- ( ph -> F = ( ~P B O B ) )
15	13 3 14	brovmptimex2	|- ( ph -> B e. _V )