Metamath Proof Explorer

Theorem ntrclsneine0lem

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that at least one (pseudo-)neighborbood of a particular point exists hold equally. (Contributed by RP, 21-May-2021)

Ref Expression
Hypotheses ntrcls.o 
|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
ntrcls.d 
|- D = ( O ` B )
ntrcls.r 
|- ( ph -> I D K )
ntrclslem0.x 
|- ( ph -> X e. B )
Assertion ntrclsneine0lem 
|- ( ph -> ( E. s e. ~P B X e. ( I ` s ) <-> E. s e. ~P B -. X e. ( K ` s ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 
 |-  O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2 ntrcls.d 
 |-  D = ( O ` B )
3 ntrcls.r 
 |-  ( ph -> I D K )
4 ntrclslem0.x 
 |-  ( ph -> X e. B )
5 fveq2 
 |-  ( s = t -> ( I ` s ) = ( I ` t ) )
6 5 eleq2d 
 |-  ( s = t -> ( X e. ( I ` s ) <-> X e. ( I ` t ) ) )
7 6 cbvrexvw 
 |-  ( E. s e. ~P B X e. ( I ` s ) <-> E. t e. ~P B X e. ( I ` t ) )
8 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ s ) e. ~P B )
9 8 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ s ) e. ~P B )
10 2 3 ntrclsrcomplex 
 |-  ( ph -> ( B \ t ) e. ~P B )
11 10 adantr 
 |-  ( ( ph /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
12 difeq2 
 |-  ( s = ( B \ t ) -> ( B \ s ) = ( B \ ( B \ t ) ) )
13 12 adantl 
 |-  ( ( ( ph /\ t e. ~P B ) /\ s = ( B \ t ) ) -> ( B \ s ) = ( B \ ( B \ t ) ) )
14 elpwi 
 |-  ( t e. ~P B -> t C_ B )
15 dfss4 
 |-  ( t C_ B <-> ( B \ ( B \ t ) ) = t )
16 14 15 sylib 
 |-  ( t e. ~P B -> ( B \ ( B \ t ) ) = t )
17 16 ad2antlr 
 |-  ( ( ( ph /\ t e. ~P B ) /\ s = ( B \ t ) ) -> ( B \ ( B \ t ) ) = t )
18 13 17 eqtr2d 
 |-  ( ( ( ph /\ t e. ~P B ) /\ s = ( B \ t ) ) -> t = ( B \ s ) )
19 11 18 rspcedeq2vd 
 |-  ( ( ph /\ t e. ~P B ) -> E. s e. ~P B t = ( B \ s ) )
20 fveq2 
 |-  ( t = ( B \ s ) -> ( I ` t ) = ( I ` ( B \ s ) ) )
21 20 eleq2d 
 |-  ( t = ( B \ s ) -> ( X e. ( I ` t ) <-> X e. ( I ` ( B \ s ) ) ) )
22 21 3ad2ant3 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( X e. ( I ` t ) <-> X e. ( I ` ( B \ s ) ) ) )
23 3 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> I D K )
24 4 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> X e. B )
25 simpr 
 |-  ( ( ph /\ s e. ~P B ) -> s e. ~P B )
26 1 2 23 24 25 ntrclselnel2 
 |-  ( ( ph /\ s e. ~P B ) -> ( X e. ( I ` ( B \ s ) ) <-> -. X e. ( K ` s ) ) )
27 26 3adant3 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( X e. ( I ` ( B \ s ) ) <-> -. X e. ( K ` s ) ) )
28 22 27 bitrd 
 |-  ( ( ph /\ s e. ~P B /\ t = ( B \ s ) ) -> ( X e. ( I ` t ) <-> -. X e. ( K ` s ) ) )
29 9 19 28 rexxfrd2 
 |-  ( ph -> ( E. t e. ~P B X e. ( I ` t ) <-> E. s e. ~P B -. X e. ( K ` s ) ) )
30 7 29 syl5bb 
 |-  ( ph -> ( E. s e. ~P B X e. ( I ` s ) <-> E. s e. ~P B -. X e. ( K ` s ) ) )