Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in interior of the complement of a set and non-membership in the closure of the set. (Contributed by RP, 28-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 ) |
||
| ntrcls.x | |- ( ph -> X e. B ) |
||
| ntrcls.s | |- ( ph -> S e. ~P B ) |
||
| Assertion | ntrclselnel2 | |- ( ph -> ( X e. ( I ` ( B \ S ) ) <-> -. X e. ( K ` S ) ) ) |
| 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 | ntrcls.x | |- ( ph -> X e. B ) |
|
| 5 | ntrcls.s | |- ( ph -> S e. ~P B ) |
|
| 6 | 1 2 3 | ntrclsnvobr | |- ( ph -> K D I ) |
| 7 | 1 2 6 4 5 | ntrclselnel1 | |- ( ph -> ( X e. ( K ` S ) <-> -. X e. ( I ` ( B \ S ) ) ) ) |
| 8 | 7 | con2bid | |- ( ph -> ( X e. ( I ` ( B \ S ) ) <-> -. X e. ( K ` S ) ) ) |