Metamath Proof Explorer

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 ffvelcdmd 
 |-  ( 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 ) =/= (/) ) )