Metamath Proof Explorer

Theorem ntrneineine1lem

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that for every point, at not all subsets are (pseudo-)neighborboods hold equally. (Contributed by RP, 1-Jun-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 ntrneineine1lem 
|- ( ph -> ( E. s e. ~P B -. X e. ( I ` s ) <-> ( N ` X ) =/= ~P 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 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 notbid 
 |-  ( ( ph /\ s e. ~P B ) -> ( -. X e. ( I ` s ) <-> -. s e. ( N ` X ) ) )
10 9 rexbidva 
 |-  ( ph -> ( E. s e. ~P B -. X e. ( I ` s ) <-> E. s e. ~P B -. s e. ( N ` X ) ) )
11 1 2 3 ntrneinex 
 |-  ( ph -> N e. ( ~P ~P B ^m B ) )
12 elmapi 
 |-  ( N e. ( ~P ~P B ^m B ) -> N : B --> ~P ~P B )
13 11 12 syl 
 |-  ( ph -> N : B --> ~P ~P B )
14 13 4 ffvelrnd 
 |-  ( ph -> ( N ` X ) e. ~P ~P B )
15 14 elpwid 
 |-  ( ph -> ( N ` X ) C_ ~P B )
16 biortn 
 |-  ( ( N ` X ) C_ ~P B -> ( -. ~P B C_ ( N ` X ) <-> ( -. ( N ` X ) C_ ~P B \/ -. ~P B C_ ( N ` X ) ) ) )
17 15 16 syl 
 |-  ( ph -> ( -. ~P B C_ ( N ` X ) <-> ( -. ( N ` X ) C_ ~P B \/ -. ~P B C_ ( N ` X ) ) ) )
18 df-rex 
 |-  ( E. s e. ~P B -. s e. ( N ` X ) <-> E. s ( s e. ~P B /\ -. s e. ( N ` X ) ) )
19 nss 
 |-  ( -. ~P B C_ ( N ` X ) <-> E. s ( s e. ~P B /\ -. s e. ( N ` X ) ) )
20 18 19 bitr4i 
 |-  ( E. s e. ~P B -. s e. ( N ` X ) <-> -. ~P B C_ ( N ` X ) )
21 df-ne 
 |-  ( ( N ` X ) =/= ~P B <-> -. ( N ` X ) = ~P B )
22 ianor 
 |-  ( -. ( ( N ` X ) C_ ~P B /\ ~P B C_ ( N ` X ) ) <-> ( -. ( N ` X ) C_ ~P B \/ -. ~P B C_ ( N ` X ) ) )
23 eqss 
 |-  ( ( N ` X ) = ~P B <-> ( ( N ` X ) C_ ~P B /\ ~P B C_ ( N ` X ) ) )
24 22 23 xchnxbir 
 |-  ( -. ( N ` X ) = ~P B <-> ( -. ( N ` X ) C_ ~P B \/ -. ~P B C_ ( N ` X ) ) )
25 21 24 bitri 
 |-  ( ( N ` X ) =/= ~P B <-> ( -. ( N ` X ) C_ ~P B \/ -. ~P B C_ ( N ` X ) ) )
26 17 20 25 3bitr4g 
 |-  ( ph -> ( E. s e. ~P B -. s e. ( N ` X ) <-> ( N ` X ) =/= ~P B ) )
27 10 26 bitrd 
 |-  ( ph -> ( E. s e. ~P B -. X e. ( I ` s ) <-> ( N ` X ) =/= ~P B ) )