Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then they are related the opposite way. (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 ) |
||
| Assertion | ntrclsnvobr | |- ( ph -> K D I ) |
| 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 | 2 3 | ntrclsbex | |- ( ph -> B e. _V ) |
| 5 | 1 2 4 | dssmapnvod | |- ( ph -> `' D = D ) |
| 6 | 1 2 3 | ntrclsf1o | |- ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) ) |
| 7 | f1orel | |- ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> Rel D ) |
|
| 8 | relbrcnvg | |- ( Rel D -> ( K `' D I <-> I D K ) ) |
|
| 9 | 6 7 8 | 3syl | |- ( ph -> ( K `' D I <-> I D K ) ) |
| 10 | 3 9 | mpbird | |- ( ph -> K `' D I ) |
| 11 | 5 10 | breqdi | |- ( ph -> K D I ) |