Theorem ntrneineine0lem

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (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 )
Assertion	ntrneineine0lem	|- ( ph -> ( E. s e. ~P B X e. ( I ` s ) <-> ( 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	3	adantr	|- ( ( ph /\ s e. ~P B ) -> I F N )
6	4	adantr	|- ( ( ph /\ s e. ~P B ) -> X e. B )
7		simpr	|- ( ( ph /\ s e. ~P B ) -> s e. ~P B )
8	1 2 5 6 7	ntrneiel	|- ( ( ph /\ s e. ~P B ) -> ( X e. ( I ` s ) <-> s e. ( N ` X ) ) )
9	8	rexbidva	|- ( ph -> ( E. s e. ~P B X e. ( I ` s ) <-> E. s e. ~P B s e. ( N ` X ) ) )
10	1 2 3	ntrneinex	|- ( ph -> N e. ( ~P ~P B ^m B ) )
11		elmapi	|- ( N e. ( ~P ~P B ^m B ) -> N : B --> ~P ~P B )
12	10 11	syl	|- ( ph -> N : B --> ~P ~P B )
13	12 4	ffvelrnd	|- ( ph -> ( N ` X ) e. ~P ~P B )
14	13	elpwid	|- ( ph -> ( N ` X ) C_ ~P B )
15	14	sseld	|- ( ph -> ( s e. ( N ` X ) -> s e. ~P B ) )
16	15	pm4.71rd	|- ( ph -> ( s e. ( N ` X ) <-> ( s e. ~P B /\ s e. ( N ` X ) ) ) )
17	16	exbidv	|- ( ph -> ( E. s s e. ( N ` X ) <-> E. s ( s e. ~P B /\ s e. ( N ` X ) ) ) )
18	17	bicomd	|- ( ph -> ( E. s ( s e. ~P B /\ s e. ( N ` X ) ) <-> E. s s e. ( N ` X ) ) )
19		df-rex	|- ( E. s e. ~P B s e. ( N ` X ) <-> E. s ( s e. ~P B /\ s e. ( N ` X ) ) )
20		n0	|- ( ( N ` X ) =/= (/) <-> E. s s e. ( N ` X ) )
21	18 19 20	3bitr4g	|- ( ph -> ( E. s e. ~P B s e. ( N ` X ) <-> ( N ` X ) =/= (/) ) )
22	9 21	bitrd	|- ( ph -> ( E. s e. ~P B X e. ( I ` s ) <-> ( N ` X ) =/= (/) ) )